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