Let X be given.
Assume HX1 HX2.
Let m be given.
Assume Hm: m ∈ ω.
Apply dneg to the current goal.
Assume H1: ¬ (∃n ∈ X, m ∈ n).
We prove the intermediate claim L1: X ⊆ ordsucc m.
Let n be given.
Assume Hn: n ∈ X.
Apply ordinal_trichotomy_or_impred m n (nat_p_ordinal m (omega_nat_p m Hm)) (nat_p_ordinal n (omega_nat_p n (HX1 n Hn))) to the current goal.
Assume H2: m ∈ n.
We will prove False.
Apply H1 to the current goal.
We use n to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hn.
An exact proof term for the current goal is H2.
Assume H2: m = n.
We will prove n ∈ ordsucc m.
rewrite the current goal using H2 (from right to left).
Apply ordsuccI2 to the current goal.
Assume H2: n ∈ m.
We will prove n ∈ ordsucc m.
Apply ordsuccI1 to the current goal.
An exact proof term for the current goal is H2.
Apply HX2 to the current goal.
We will prove finite X.
An exact proof term for the current goal is Subq_finite (ordsucc m) (nat_finite (ordsucc m) (nat_ordsucc m (omega_nat_p m Hm))) X L1.
∎