Let alpha be given.

Assume Ha: ordinal alpha.

We will prove ∃beta, ordinal beta ∧ SNo_ beta alpha.

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

∎