Let α be given.
Assume Ha.
Apply xm (∃β ∈ α, α = ordsucc β) to the current goal.
Assume H1.
Apply orIR to the current goal.
An exact proof term for the current goal is H1.
Assume H1: ¬ ∃β ∈ α, α = ordsucc β.
Apply orIL to the current goal.
Let β be given.
Assume H2: β ∈ α.
Apply ordinal_ordsucc_In_eq α β Ha H2 to the current goal.
Assume H3: ordsucc β ∈ α.
An exact proof term for the current goal is H3.
Assume H3: α = ordsucc β.
We will prove False.
Apply H1 to the current goal.
We use β to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is H2.
An exact proof term for the current goal is H3.
∎