An exact proof term for the current goal is (λn H1 p H2 H3 ⇒ H3 n (H1 p H2 H3)).