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