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