An exact proof term for the current goal is (λu ⇒ orIL (P1 ∨ P2) P3 (orIR P1 P2 u)).