Let n and y be given.
Assume HnO: n ∈ ω.
Assume HyX: y ∈ setprod 2 ω.
Assume H1n_y: order_rel (setprod 2 ω) (1,n) y.
Assume Hy_1sn: order_rel (setprod 2 ω) y (1,ordsucc n).
Set X to be the term setprod 2 ω.
We prove the intermediate claim Hex1: ∃i m j t : set, i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ t ∈ ω ∧ (1,n) = (i,m) ∧ y = (j,t) ∧ (i ∈ j ∨ (i = j ∧ m ∈ t)).
An exact proof term for the current goal is (order_rel_setprod_2_omega_unfold (1,n) y H1n_y).
We prove the intermediate claim Hex2: ∃i2 m2 j2 t2 : set, i2 ∈ 2 ∧ m2 ∈ ω ∧ j2 ∈ 2 ∧ t2 ∈ ω ∧ y = (i2,m2) ∧ (1,ordsucc n) = (j2,t2) ∧ (i2 ∈ j2 ∨ (i2 = j2 ∧ m2 ∈ t2)).
An exact proof term for the current goal is (order_rel_setprod_2_omega_unfold y (1,ordsucc n) Hy_1sn).
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 t be given.
Assume Hcore1: (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ t ∈ ω ∧ (1,n) = (i,m) ∧ y = (j,t) ∧ (i ∈ j ∨ (i = j ∧ m ∈ t))).
Apply (and7E (i ∈ 2) (m ∈ ω) (j ∈ 2) (t ∈ ω) ((1,n) = (i,m)) (y = (j,t)) (i ∈ j ∨ (i = j ∧ m ∈ t)) Hcore1 False) to the current goal.
Assume Hi2 HmO Hj2 HtO H1nEq HyEq1 Hlex1.
We prove the intermediate claim H1i: 1 = i.
An exact proof term for the current goal is (pair_eq_fst 1 n i m H1nEq).
We prove the intermediate claim Hi1: i = 1.
Use symmetry.
An exact proof term for the current goal is H1i.
We prove the intermediate claim Hnm: n = m.
An exact proof term for the current goal is (pair_eq_snd 1 n i m H1nEq).
We prove the intermediate claim HmN: m = n.
Use symmetry.
An exact proof term for the current goal is Hnm.
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 t2 be given.
Assume Hcore2: (i2 ∈ 2 ∧ m2 ∈ ω ∧ j2 ∈ 2 ∧ t2 ∈ ω ∧ y = (i2,m2) ∧ (1,ordsucc n) = (j2,t2) ∧ (i2 ∈ j2 ∨ (i2 = j2 ∧ m2 ∈ t2))).
Apply (and7E (i2 ∈ 2) (m2 ∈ ω) (j2 ∈ 2) (t2 ∈ ω) (y = (i2,m2)) ((1,ordsucc n) = (j2,t2)) (i2 ∈ j2 ∨ (i2 = j2 ∧ m2 ∈ t2)) Hcore2 False) to the current goal.
Assume Hi2_2 Hm2O Hj2_2 Ht2O HyEq2 H1snEq Hlex2.
We prove the intermediate claim H1j2: 1 = j2.
An exact proof term for the current goal is (pair_eq_fst 1 (ordsucc n) j2 t2 H1snEq).
We prove the intermediate claim Hj21: j2 = 1.
Use symmetry.
An exact proof term for the current goal is H1j2.
We prove the intermediate claim Hsn_t2: ordsucc n = t2.
An exact proof term for the current goal is (pair_eq_snd 1 (ordsucc n) j2 t2 H1snEq).
We prove the intermediate claim Ht2EqSn: t2 = ordsucc n.
Use symmetry.
An exact proof term for the current goal is Hsn_t2.
Apply Hlex2 to the current goal.
Assume Hi2Inj2: i2 ∈ j2.
We prove the intermediate claim Hi2In1: i2 ∈ 1.
We will prove i2 ∈ 1.
rewrite the current goal using Hj21 (from right to left).
An exact proof term for the current goal is Hi2Inj2.
Apply (ordsuccE 0 i2 Hi2In1 False) to the current goal.
Assume Hi2In0: i2 ∈ 0.
An exact proof term for the current goal is (EmptyE i2 Hi2In0).
Assume Hi20: i2 = 0.
We prove the intermediate claim HeqPairs: (j,t) = (i2,m2).
We will prove (j,t) = (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 t 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.
Apply Hlex1 to the current goal.
Assume Hij: i ∈ j.
We prove the intermediate claim H1in0: 1 ∈ 0.
We will prove 1 ∈ 0.
rewrite the current goal using Hi1 (from right to left).
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 1 H1in0).
Assume Hconj1: i = j ∧ m ∈ t.
We prove the intermediate claim HijEq: i = j.
An exact proof term for the current goal is (andEL (i = j) (m ∈ t) Hconj1).
We prove the intermediate claim H10: 1 = 0.
We will prove 1 = 0.
rewrite the current goal using Hi1 (from right to left) at position 1.
rewrite the current goal using Hj0 (from right to left).
An exact proof term for the current goal is HijEq.
We prove the intermediate claim H01: 0 = 1.
Use symmetry.
An exact proof term for the current goal is H10.
An exact proof term for the current goal is (neq_0_1 H01).
Assume Hconj2: i2 = j2 ∧ m2 ∈ t2.
We prove the intermediate claim Hi2Eqj2: i2 = j2.
An exact proof term for the current goal is (andEL (i2 = j2) (m2 ∈ t2) Hconj2).
We prove the intermediate claim Hm2InT2: m2 ∈ t2.
An exact proof term for the current goal is (andER (i2 = j2) (m2 ∈ t2) Hconj2).
We prove the intermediate claim Hi21: i2 = 1.
We will prove i2 = 1.
rewrite the current goal using Hi2Eqj2 (from left to right).
An exact proof term for the current goal is Hj21.
We prove the intermediate claim Hm2InSn: m2 ∈ ordsucc n.
We will prove m2 ∈ ordsucc n.
rewrite the current goal using Ht2EqSn (from right to left).
An exact proof term for the current goal is Hm2InT2.
We prove the intermediate claim HeqPairs: (j,t) = (i2,m2).
We will prove (j,t) = (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 t i2 m2 HeqPairs).
We prove the intermediate claim HtEqM2: t = m2.
An exact proof term for the current goal is (pair_eq_snd j t i2 m2 HeqPairs).
We prove the intermediate claim Hj1: j = 1.
We will prove j = 1.
rewrite the current goal using HjEqI2 (from left to right).
An exact proof term for the current goal is Hi21.
We prove the intermediate claim HtInSn: t ∈ ordsucc n.
We will prove t ∈ ordsucc n.
rewrite the current goal using HtEqM2 (from left to right).
An exact proof term for the current goal is Hm2InSn.
Apply Hlex1 to the current goal.
Assume Hij: i ∈ j.
We prove the intermediate claim H1in1: 1 ∈ 1.
We will prove 1 ∈ 1.
rewrite the current goal using Hi1 (from right to left) at position 1.
rewrite the current goal using Hj1 (from right to left).
An exact proof term for the current goal is Hij.
An exact proof term for the current goal is (In_no2cycle 1 1 H1in1 H1in1).
Assume Hconj1: i = j ∧ m ∈ t.
We prove the intermediate claim HmInT: m ∈ t.
An exact proof term for the current goal is (andER (i = j) (m ∈ t) Hconj1).
We prove the intermediate claim HnInT: n ∈ t.
We will prove n ∈ t.
rewrite the current goal using HmN (from right to left).
An exact proof term for the current goal is HmInT.
Apply (ordsuccE n t HtInSn False) to the current goal.
Assume HtInN: t ∈ n.
An exact proof term for the current goal is (In_no2cycle n t HnInT HtInN).
Assume HtEqN: t = n.
We prove the intermediate claim HnInN: n ∈ n.
We will prove n ∈ n.
rewrite the current goal using HtEqN (from right to left) at position 2.
An exact proof term for the current goal is HnInT.
An exact proof term for the current goal is (In_no2cycle n n HnInN HnInN).
∎