Let p be given.

Assume H1.

Apply dneg to the current goal.

Assume H2: ¬ ∃α, ordinal α ∧ p α ∧ ∀β ∈ α, ¬ p β.

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

Apply ordinal_ind to the current goal.

Let α be given.

Assume Ha.

Assume IH: ∀β ∈ α, ¬ p β.

Assume H3: p α.

Apply H2 to the current goal.

We use α 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 α be given.

Assume H1a.

Apply H1a to the current goal.

Assume Ha: ordinal α.

Assume Hp: p α.

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

∎