Let X, a and b be given.
Assume Hwo: well_ordered_set X.
Assume Hrel: order_rel X a b.
We will prove a ∈ b.
Set T0 to be the term ordinal X ∧ X ≠ R.
Set T1 to be the term T0 ∧ X ≠ rational_numbers.
Set T2 to be the term T1 ∧ X ≠ setprod 2 ω.
Set T3 to be the term T2 ∧ X ≠ setprod R R.
We prove the intermediate claim HT3: T3.
An exact proof term for the current goal is Hwo.
We prove the intermediate claim HT2: T2.
An exact proof term for the current goal is (andEL T2 (X ≠ setprod R R) HT3).
We prove the intermediate claim HneqRR: X ≠ setprod R R.
An exact proof term for the current goal is (andER T2 (X ≠ setprod R R) HT3).
We prove the intermediate claim HT1: T1.
An exact proof term for the current goal is (andEL T1 (X ≠ setprod 2 ω) HT2).
We prove the intermediate claim Hneq2omega: X ≠ setprod 2 ω.
An exact proof term for the current goal is (andER T1 (X ≠ setprod 2 ω) HT2).
We prove the intermediate claim HT0: T0.
An exact proof term for the current goal is (andEL T0 (X ≠ rational_numbers) HT1).
We prove the intermediate claim HneqRat: X ≠ rational_numbers.
An exact proof term for the current goal is (andER T0 (X ≠ rational_numbers) HT1).
We prove the intermediate claim Hord: ordinal X.
An exact proof term for the current goal is (andEL (ordinal X) (X ≠ R) HT0).
We prove the intermediate claim HneqR: X ≠ R.
An exact proof term for the current goal is (andER (ordinal X) (X ≠ R) HT0).
Apply (Hrel (a ∈ b)) to the current goal.
Assume Hleft6.
Apply (Hleft6 (a ∈ b)) to the current goal.
Assume Hleft.
Apply (Hleft (a ∈ b)) to the current goal.
Assume Hleft2.
Apply (Hleft2 (a ∈ b)) to the current goal.
Assume Hleft3.
Apply (Hleft3 (a ∈ b)) to the current goal.
Assume Hleft4.
Apply (Hleft4 (a ∈ b)) to the current goal.
Assume HA: X = R ∧ Rlt a b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = R.
An exact proof term for the current goal is (andEL (X = R) (Rlt a b) HA).
An exact proof term for the current goal is (HneqR Heq).
Assume HB: X = rational_numbers ∧ Rlt a b.
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = rational_numbers.
An exact proof term for the current goal is (andEL (X = rational_numbers) (Rlt a b) HB).
An exact proof term for the current goal is (HneqRat Heq).
Assume HC: X = ω ∧ a ∈ b.
An exact proof term for the current goal is (andER (X = ω) (a ∈ b) HC).
Assume HD: X = ω ∖ {0} ∧ a ∈ b.
An exact proof term for the current goal is (andER (X = ω ∖ {0}) (a ∈ b) HD).
Assume HE: X = setprod 2 ω ∧ ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = setprod 2 ω.
An exact proof term for the current goal is (andEL (X = setprod 2 ω) (∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ a = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))) HE).
An exact proof term for the current goal is (Hneq2omega Heq).
Assume HF: X = setprod R R ∧ ∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).
Apply FalseE to the current goal.
We prove the intermediate claim Heq: X = setprod R R.
An exact proof term for the current goal is (andEL (X = setprod R R) (∃a1 a2 b1 b2 : set, a = (a1,a2) ∧ b = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2))) HF).
An exact proof term for the current goal is (HneqRR Heq).
Assume Hord: ordinal X ∧ X ≠ R ∧ X ≠ rational_numbers ∧ X ≠ setprod 2 ω ∧ X ≠ setprod R R ∧ a ∈ b.
An exact proof term for the current goal is (andER (ordinal X ∧ X ≠ R ∧ X ≠ rational_numbers ∧ X ≠ setprod 2 ω ∧ X ≠ setprod R R) (a ∈ b) Hord).
∎