Let k and y be given.
Assume HkO: k ∈ ω.
Assume HyX: y ∈ setprod 2 ω.
Assume H0k_y: order_rel (setprod 2 ω) (0,k) y.
Assume Hy_0sk: order_rel (setprod 2 ω) y (0,ordsucc k).
Set X to be the term setprod 2 ω.
We prove the intermediate claim Hex1: ∃i m j n : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (0,k) = (i,m) ∧ y = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
An exact proof term for the current goal is (order_rel_setprod_2_omega_unfold (0,k) y H0k_y).
We prove the intermediate claim Hex2: ∃i2 m2 j2 n2 : set, i2 ∈ 2 ∧ m2 ∈ ω ∧ j2 ∈ 2 ∧ n2 ∈ ω ∧ y = (i2,m2) ∧ (0,ordsucc k) = (j2,n2) ∧ (i2 ∈ j2 ∨ (i2 = j2 ∧ m2 ∈ n2)).
An exact proof term for the current goal is (order_rel_setprod_2_omega_unfold y (0,ordsucc k) Hy_0sk).
Apply Hex1 to the current goal.
Let i be given.
Assume HiPair.
Apply HiPair to the current goal.
Let m be given.
Assume HmPair.
Apply HmPair to the current goal.
Let j be given.
Assume HjPair.
Apply HjPair to the current goal.
Let n be given.
Assume Hcore1: (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ (0,k) = (i,m) ∧ y = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))).
Apply (and7E (i ∈ 2) (m ∈ ω) (j ∈ 2) (n ∈ ω) ((0,k) = (i,m)) (y = (j,n)) (i ∈ j ∨ (i = j ∧ m ∈ n)) Hcore1 False) to the current goal.
Assume Hi2 HmO Hj2 HnO H0kEq HyEq1 Hlex1.
We prove the intermediate claim H0i: 0 = i.
An exact proof term for the current goal is (pair_eq_fst 0 k i m H0kEq).
We prove the intermediate claim Hi0: i = 0.
Use symmetry.
An exact proof term for the current goal is H0i.
We prove the intermediate claim Hkm: k = m.
An exact proof term for the current goal is (pair_eq_snd 0 k i m H0kEq).
We prove the intermediate claim HmK: m = k.
Use symmetry.
An exact proof term for the current goal is Hkm.
Apply Hex2 to the current goal.
Let i2 be given.
Assume Hi2Pair.
Apply Hi2Pair to the current goal.
Let m2 be given.
Assume Hm2Pair.
Apply Hm2Pair to the current goal.
Let j2 be given.
Assume Hj2Pair.
Apply Hj2Pair to the current goal.
Let n2 be given.
Assume Hcore2: (i2 ∈ 2 ∧ m2 ∈ ω ∧ j2 ∈ 2 ∧ n2 ∈ ω ∧ y = (i2,m2) ∧ (0,ordsucc k) = (j2,n2) ∧ (i2 ∈ j2 ∨ (i2 = j2 ∧ m2 ∈ n2))).
Apply (and7E (i2 ∈ 2) (m2 ∈ ω) (j2 ∈ 2) (n2 ∈ ω) (y = (i2,m2)) ((0,ordsucc k) = (j2,n2)) (i2 ∈ j2 ∨ (i2 = j2 ∧ m2 ∈ n2)) Hcore2 False) to the current goal.
Assume Hi2_2 Hm2O Hj2_2 Hn2O HyEq2 H0skEq Hlex2.
We prove the intermediate claim H0j2: 0 = j2.
An exact proof term for the current goal is (pair_eq_fst 0 (ordsucc k) j2 n2 H0skEq).
We prove the intermediate claim Hj20: j2 = 0.
Use symmetry.
An exact proof term for the current goal is H0j2.
We prove the intermediate claim Hsk_n2: ordsucc k = n2.
An exact proof term for the current goal is (pair_eq_snd 0 (ordsucc k) j2 n2 H0skEq).
We prove the intermediate claim Hn2EqSk: n2 = ordsucc k.
Use symmetry.
An exact proof term for the current goal is Hsk_n2.
Apply Hlex2 to the current goal.
Assume Hi2Inj2: i2 ∈ j2.
We prove the intermediate claim Hi2In0: i2 ∈ 0.
We will prove i2 ∈ 0.
rewrite the current goal using Hj20 (from right to left).
An exact proof term for the current goal is Hi2Inj2.
An exact proof term for the current goal is (EmptyE i2 Hi2In0).
Assume Hconj2: i2 = j2 ∧ m2 ∈ n2.
We prove the intermediate claim Hi2Eqj2: i2 = j2.
An exact proof term for the current goal is (andEL (i2 = j2) (m2 ∈ n2) Hconj2).
We prove the intermediate claim Hm2InN2: m2 ∈ n2.
An exact proof term for the current goal is (andER (i2 = j2) (m2 ∈ n2) Hconj2).
We prove the intermediate claim Hi20: i2 = 0.
We will prove i2 = 0.
rewrite the current goal using Hi2Eqj2 (from left to right).
An exact proof term for the current goal is Hj20.
We prove the intermediate claim Hm2InSk: m2 ∈ ordsucc k.
We will prove m2 ∈ ordsucc k.
rewrite the current goal using Hn2EqSk (from right to left).
An exact proof term for the current goal is Hm2InN2.
We prove the intermediate claim HeqPairs: (j,n) = (i2,m2).
We will prove (j,n) = (i2,m2).
rewrite the current goal using HyEq1 (from right to left).
An exact proof term for the current goal is HyEq2.
We prove the intermediate claim HjEqI2: j = i2.
An exact proof term for the current goal is (pair_eq_fst j n i2 m2 HeqPairs).
We prove the intermediate claim HnEqM2: n = m2.
An exact proof term for the current goal is (pair_eq_snd j n i2 m2 HeqPairs).
We prove the intermediate claim Hj0: j = 0.
We will prove j = 0.
rewrite the current goal using HjEqI2 (from left to right).
An exact proof term for the current goal is Hi20.
We prove the intermediate claim HnInSk: n ∈ ordsucc k.
We will prove n ∈ ordsucc k.
rewrite the current goal using HnEqM2 (from left to right).
An exact proof term for the current goal is Hm2InSk.
Apply Hlex1 to the current goal.
Assume Hij: i ∈ j.
We prove the intermediate claim HiIn0: i ∈ 0.
We will prove i ∈ 0.
rewrite the current goal using Hj0 (from right to left).
An exact proof term for the current goal is Hij.
An exact proof term for the current goal is (EmptyE i HiIn0).
Assume Hconj1: i = j ∧ m ∈ n.
We prove the intermediate claim HmInN: m ∈ n.
An exact proof term for the current goal is (andER (i = j) (m ∈ n) Hconj1).
We prove the intermediate claim HkInN: k ∈ n.
We will prove k ∈ n.
rewrite the current goal using HmK (from right to left).
An exact proof term for the current goal is HmInN.
Apply (ordsuccE k n HnInSk False) to the current goal.
Assume HnInK: n ∈ k.
An exact proof term for the current goal is (In_no2cycle k n HkInN HnInK).
Assume HnEqK: n = k.
We prove the intermediate claim HkInK: k ∈ k.
We will prove k ∈ k.
rewrite the current goal using HnEqK (from right to left) at position 2.
An exact proof term for the current goal is HkInN.
An exact proof term for the current goal is (In_no2cycle k k HkInK HkInK).
∎