Let X be given.
Assume Hwo: well_ordered_set X.
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 HT1: T1.
An exact proof term for the current goal is (andEL 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).
An exact proof term for the current goal is (andEL (ordinal X) (X ≠ R) HT0).
∎