Apply SNoCutP_L_0 to the current goal.

Let x be given.

Assume Hx.

We will prove False.

An exact proof term for the current goal is EmptyE x Hx.

∎