Let P be given.

Apply Empty_eq to the current goal.

Let x be given.

Assume Hx.

An exact proof term for the current goal is EmptyE x (SepE1 Empty P x Hx).

∎