Let P be given.

Assume H1.

Apply xm P to the current goal.

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

Assume H2: ¬ P.

We will prove False.

An exact proof term for the current goal is H1 H2.

∎