An exact proof term for the current goal is (λH1 H2 H3 ⇒ andI (P1 ∧ P2) P3 (andI P1 P2 H1 H2) H3).