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