Let α be given.

Assume Ha: ordinal α.

We will prove ∃β, ordinal β ∧ SNo_ β α.

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 ordinal_SNo_ α Ha.

∎