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