Let alpha be given.

Assume Ha.

Let z be given.

Assume Hz: SNo_ alpha z.

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

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

∎