Let α be given.

Assume Ha: ordinal α.

Let p be given.

We prove the intermediate claim L1: SNo_ α (PSNo α p).

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

We prove the intermediate claim L2: SNo (PSNo α p).

We will prove ∃β, ordinal β ∧ SNo_ β (PSNo α p).

We use α to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is L1.

Apply SNoLev_prop (PSNo α p) L2 to the current goal.

Assume H2: ordinal (SNoLev (PSNo α p)).

Assume H3: SNo_ (SNoLev (PSNo α p)) (PSNo α p).

An exact proof term for the current goal is SNoLev_uniq (PSNo α p) (SNoLev (PSNo α p)) α H2 Ha H3 L1.

∎