An exact proof term for the current goal is (λA B a P H1 H2 ⇒ H1 a).