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