Let p be given.

Assume H1.

Apply dneg to the current goal.

Assume H2: ¬ ∃alpha, ordinal alpha ∧ p alpha ∧ ∀beta ∈ alpha, ¬ p beta.

We prove the intermediate claim L1: ∀alpha, ordinal alpha → ¬ p alpha.

Apply ordinal_ind to the current goal.

Let alpha be given.

Assume Ha.

Assume IH: ∀beta ∈ alpha, ¬ p beta.

Assume H3: p alpha.

Apply H2 to the current goal.

We use alpha to witness the existential quantifier.

Apply and3I to the current goal.

An exact proof term for the current goal is Ha.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is IH.

Apply H1 to the current goal.

Let alpha be given.

Assume H1a.

Apply H1a to the current goal.

Assume Ha: ordinal alpha.

Assume Hp: p alpha.

An exact proof term for the current goal is L1 alpha Ha Hp.

∎