Let a and b be given.
Assume Ha: a ∈ ω.
Assume Hb: b ∈ ω.
We will prove a ∪ b ∈ ω.
Apply (xm (a ∈ b)) to the current goal.
Assume Hab: a ∈ b.
We prove the intermediate claim Hsub: a ⊆ b.
We prove the intermediate claim Hb_nat: nat_p b.
An exact proof term for the current goal is (omega_nat_p b Hb).
We prove the intermediate claim Hb_ord: ordinal b.
An exact proof term for the current goal is (nat_p_ordinal b Hb_nat).
We prove the intermediate claim Hb_trans: TransSet b.
An exact proof term for the current goal is (andEL (TransSet b) (∀beta ∈ b, TransSet beta) Hb_ord).
An exact proof term for the current goal is (Hb_trans a Hab).
We prove the intermediate claim Heq: a ∪ b = b.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binunion_Subq_min a b b Hsub (Subq_ref b)).
An exact proof term for the current goal is (binunion_Subq_2 a b).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hb.
Assume Hanb: a ∉ b.
We prove the intermediate claim Ha_nat: nat_p a.
An exact proof term for the current goal is (omega_nat_p a Ha).
We prove the intermediate claim Hb_nat: nat_p b.
An exact proof term for the current goal is (omega_nat_p b Hb).
We prove the intermediate claim Ha_ord: ordinal a.
An exact proof term for the current goal is (nat_p_ordinal a Ha_nat).
We prove the intermediate claim Hb_ord: ordinal b.
An exact proof term for the current goal is (nat_p_ordinal b Hb_nat).
We prove the intermediate claim Hcases: a ∈ b ∨ b ⊆ a.
An exact proof term for the current goal is (ordinal_In_Or_Subq a b Ha_ord Hb_ord).
We prove the intermediate claim Hsub: b ⊆ a.
Apply (Hcases (b ⊆ a)) to the current goal.
Assume Hab: a ∈ b.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hanb Hab).
Assume H.
An exact proof term for the current goal is H.
We prove the intermediate claim Heq: a ∪ b = a.
Apply set_ext to the current goal.
An exact proof term for the current goal is (binunion_Subq_min a b a (Subq_ref a) Hsub).
An exact proof term for the current goal is (binunion_Subq_1 a b).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Ha.
∎