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