Let x be given.

Assume Hx Hx0.

Apply SNo_eq x 0 Hx SNo_0 to the current goal.

We will prove SNoLev x = SNoLev 0.

rewrite the current goal using SNoLev_0 (from left to right).

An exact proof term for the current goal is Hx0.

We will prove SNoEq_ (SNoLev x) x 0.

rewrite the current goal using Hx0 (from left to right).

Let α be given.

Assume Ha: α ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE α Ha.

∎