Let alpha be given.

Assume Ha.

Let x be given.

Assume Hx.

Apply SNoLev_prop x (SNo_SNo alpha Ha x Hx) to the current goal.

Assume Hx1: ordinal (SNoLev x).

Assume Hx2: SNo_ (SNoLev x) x.

Apply SNoLev_uniq x to the current goal.

An exact proof term for the current goal is Hx1.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is Hx2.

An exact proof term for the current goal is Hx.

∎