Let α be given.

Assume Ha.

Let z be given.

Assume Hz: SNo_ α z.

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

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 Hz.

∎