An exact proof term for the current goal is (λp H _ ⇒ H).