Let alpha be given.

Assume Ha: ordinal alpha.

Let p be given.

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

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

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

We will prove ∃beta, ordinal beta ∧ SNo_ beta (PSNo alpha p).

We use alpha 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 alpha p) L2 to the current goal.

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

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

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

∎