Set X to be the term two_by_nat.
Set U to be the term {(1,0)}.
Assume HU: U ∈ order_topology_basis X.
We will prove False.
Set A to be the term {I ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I = {x ∈ X|order_rel X a x ∧ order_rel X x b}}.
Set B to be the term {I ∈ đ’Ģ X|∃b ∈ X, I = {x ∈ X|order_rel X x b}}.
Set C to be the term {I ∈ đ’Ģ X|∃a ∈ X, I = {x ∈ X|order_rel X a x}}.
Set Bold to be the term (A âˆĒ B âˆĒ C).
We prove the intermediate claim HUold: U ∈ Bold.
We prove the intermediate claim HUin: U ∈ (Bold âˆĒ {X}).
We prove the intermediate claim Hdef: order_topology_basis X = (Bold âˆĒ {X}).
Use reflexivity.
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is HU.
Apply (binunionE Bold {X} U HUin) to the current goal.
Assume HUbold: U ∈ Bold.
An exact proof term for the current goal is HUbold.
Assume HUX: U ∈ {X}.
Apply FalseE to the current goal.
We prove the intermediate claim HUeqX: U = X.
An exact proof term for the current goal is (SingE X U HUX).
We prove the intermediate claim H0omega: 0 ∈ Ī‰.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H00X: (0,0) ∈ X.
We prove the intermediate claim HXeq: X = setprod 2 Ī‰.
Use reflexivity.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 Ī‰ 0 0 In_0_2 H0omega).
We prove the intermediate claim H00U: (0,0) ∈ U.
rewrite the current goal using HUeqX (from left to right).
An exact proof term for the current goal is H00X.
We prove the intermediate claim H00Eq10: (0,0) = (1,0).
An exact proof term for the current goal is (SingE (1,0) (0,0) H00U).
We prove the intermediate claim H0Eq1: 0 = 1.
We will prove 0 = 1.
rewrite the current goal using (tuple_2_0_eq 0 0) (from right to left) at position 1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left) at position 2.
We prove the intermediate claim Hproj0: (0,0) 0 = (1,0) 0.
rewrite the current goal using H00Eq10 (from left to right).
Use reflexivity.
An exact proof term for the current goal is Hproj0.
An exact proof term for the current goal is (neq_0_1 H0Eq1).
Apply (binunionE' ({I ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I = {x ∈ X|order_rel X a x ∧ order_rel X x b}} âˆĒ {I ∈ đ’Ģ X|∃b ∈ X, I = {x ∈ X|order_rel X x b}}) {I ∈ đ’Ģ X|∃a ∈ X, I = {x ∈ X|order_rel X a x}} U False) to the current goal.
Assume HU12: U ∈ ({I ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I = {x ∈ X|order_rel X a x ∧ order_rel X x b}} âˆĒ {I ∈ đ’Ģ X|∃b ∈ X, I = {x ∈ X|order_rel X x b}}).
Apply (binunionE' {I ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I = {x ∈ X|order_rel X a x ∧ order_rel X x b}} {I ∈ đ’Ģ X|∃b ∈ X, I = {x ∈ X|order_rel X x b}} U False) to the current goal.
Assume HU1: U ∈ {I ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I = {x ∈ X|order_rel X a x ∧ order_rel X x b}}.
We prove the intermediate claim Hexab: ∃a ∈ X, ∃b ∈ X, U = {x ∈ X|order_rel X a x ∧ order_rel X x b}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}) U HU1).
Apply Hexab to the current goal.
Let a be given.
Assume HaPair.
Apply HaPair to the current goal.
Assume HaX: a ∈ X.
Assume Hexb.
Apply Hexb to the current goal.
Let b be given.
Assume HbPair.
Apply HbPair to the current goal.
Assume HbX: b ∈ X.
Assume HUeq: U = {x ∈ X|order_rel X a x ∧ order_rel X x b}.
We prove the intermediate claim H10inU: (1,0) ∈ U.
An exact proof term for the current goal is (SingI (1,0)).
We prove the intermediate claim H10inDef: (1,0) ∈ {x ∈ X|order_rel X a x ∧ order_rel X x b}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is H10inU.
We prove the intermediate claim Hrelconj: order_rel X a (1,0) ∧ order_rel X (1,0) b.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) (1,0) H10inDef).
We prove the intermediate claim HrelL: order_rel X a (1,0).
An exact proof term for the current goal is (andEL (order_rel X a (1,0)) (order_rel X (1,0) b) Hrelconj).
We prove the intermediate claim HrelR: order_rel X (1,0) b.
An exact proof term for the current goal is (andER (order_rel X a (1,0)) (order_rel X (1,0) b) Hrelconj).
We prove the intermediate claim HXeq: X = setprod 2 Ī‰.
Use reflexivity.
We prove the intermediate claim HrelL2: order_rel (setprod 2 Ī‰) a (1,0).
We will prove order_rel (setprod 2 Ī‰) a (1,0).
rewrite the current goal using HXeq (from right to left) at position 1.
An exact proof term for the current goal is HrelL.
We prove the intermediate claim HrelR2: order_rel (setprod 2 Ī‰) (1,0) b.
We will prove order_rel (setprod 2 Ī‰) (1,0) b.
rewrite the current goal using HXeq (from right to left) at position 1.
An exact proof term for the current goal is HrelR.
We prove the intermediate claim HexL: ∃i m j n0 : set, i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n0 ∈ Ī‰ ∧ a = (i,m) ∧ (1,0) = (j,n0) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n0)).
An exact proof term for the current goal is (order_rel_setprod_2_omega_unfold a (1,0) HrelL2).
Apply HexL 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 n0 be given.
Assume Hcore.
We prove the intermediate claim Hcoords: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n0 ∈ Ī‰ ∧ a = (i,m) ∧ (1,0) = (j,n0).
Apply Hcore to the current goal.
Assume Hcoords0 Hlex0.
An exact proof term for the current goal is Hcoords0.
We prove the intermediate claim Hlex: i ∈ j ∨ (i = j ∧ m ∈ n0).
Apply Hcore to the current goal.
Assume Hcoords0 Hlex0.
An exact proof term for the current goal is Hlex0.
We prove the intermediate claim HjnEq: (1,0) = (j,n0).
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n0 ∈ Ī‰ ∧ a = (i,m)) ((1,0) = (j,n0)) Hcoords).
We prove the intermediate claim Hcoords5: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n0 ∈ Ī‰ ∧ a = (i,m).
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n0 ∈ Ī‰ ∧ a = (i,m)) ((1,0) = (j,n0)) Hcoords).
We prove the intermediate claim HaEq2: a = (i,m).
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n0 ∈ Ī‰) (a = (i,m)) Hcoords5).
We prove the intermediate claim Hcoords4: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n0 ∈ Ī‰.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n0 ∈ Ī‰) (a = (i,m)) Hcoords5).
We prove the intermediate claim Hn0Omega: n0 ∈ Ī‰.
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2) (n0 ∈ Ī‰) Hcoords4).
We prove the intermediate claim Hcoords3: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2) (n0 ∈ Ī‰) Hcoords4).
We prove the intermediate claim Hj2: j ∈ 2.
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰) (j ∈ 2) Hcoords3).
We prove the intermediate claim Hcoords2: i ∈ 2 ∧ m ∈ Ī‰.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰) (j ∈ 2) Hcoords3).
We prove the intermediate claim Hi2: i ∈ 2.
An exact proof term for the current goal is (andEL (i ∈ 2) (m ∈ Ī‰) Hcoords2).
We prove the intermediate claim HmOmega: m ∈ Ī‰.
An exact proof term for the current goal is (andER (i ∈ 2) (m ∈ Ī‰) Hcoords2).
We prove the intermediate claim HjEq1: j = 1.
We will prove j = 1.
rewrite the current goal using (tuple_2_0_eq j n0) (from right to left) at position 1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left) at position 2.
We prove the intermediate claim Hproj0: (j,n0) 0 = (1,0) 0.
rewrite the current goal using HjnEq (from right to left).
Use reflexivity.
An exact proof term for the current goal is Hproj0.
We prove the intermediate claim Hn0Eq0: n0 = 0.
We will prove n0 = 0.
rewrite the current goal using (tuple_2_1_eq j n0) (from right to left) at position 1.
rewrite the current goal using HjnEq (from right to left) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq 1 0).
We prove the intermediate claim HiEq0: i = 0.
Apply (Hlex (i = 0)) to the current goal.
Assume Hilj: i ∈ j.
We will prove i = 0.
We prove the intermediate claim HiIn1: i ∈ 1.
rewrite the current goal using HjEq1 (from right to left).
An exact proof term for the current goal is Hilj.
We prove the intermediate claim HiInSing0: i ∈ {0}.
rewrite the current goal using eq_1_Sing0 (from right to left).
An exact proof term for the current goal is HiIn1.
An exact proof term for the current goal is (SingE 0 i HiInSing0).
Assume Hind: i = j ∧ m ∈ n0.
Apply FalseE to the current goal.
We prove the intermediate claim Hmn: m ∈ n0.
An exact proof term for the current goal is (andER (i = j) (m ∈ n0) Hind).
We prove the intermediate claim HmIn0: m ∈ 0.
rewrite the current goal using Hn0Eq0 (from right to left).
An exact proof term for the current goal is Hmn.
An exact proof term for the current goal is (EmptyE m HmIn0).
We prove the intermediate claim HaEq: a = (0,m).
We will prove a = (0,m).
rewrite the current goal using HaEq2 (from left to right).
rewrite the current goal using HiEq0 (from left to right).
Use reflexivity.
We prove the intermediate claim HexR: ∃i2 m2 j2 n : set, i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i2,m2) ∧ b = (j2,n) ∧ (i2 ∈ j2 ∨ (i2 = j2 ∧ m2 ∈ n)).
An exact proof term for the current goal is (order_rel_setprod_2_omega_unfold (1,0) b HrelR2).
Apply HexR 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 n be given.
Assume Hcore2.
We prove the intermediate claim HcoordsR: i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i2,m2) ∧ b = (j2,n).
Apply Hcore2 to the current goal.
Assume Hcoords0 Hlex0.
An exact proof term for the current goal is Hcoords0.
We prove the intermediate claim HlexR: i2 ∈ j2 ∨ (i2 = j2 ∧ m2 ∈ n).
Apply Hcore2 to the current goal.
Assume Hcoords0 Hlex0.
An exact proof term for the current goal is Hlex0.
We prove the intermediate claim HbEq2: b = (j2,n).
An exact proof term for the current goal is (andER (i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i2,m2)) (b = (j2,n)) HcoordsR).
We prove the intermediate claim HcoordsR5: i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i2,m2).
An exact proof term for the current goal is (andEL (i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i2,m2)) (b = (j2,n)) HcoordsR).
We prove the intermediate claim H10EqR: (1,0) = (i2,m2).
An exact proof term for the current goal is (andER (i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2 ∧ n ∈ Ī‰) ((1,0) = (i2,m2)) HcoordsR5).
We prove the intermediate claim HcoordsR4: i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2 ∧ n ∈ Ī‰.
An exact proof term for the current goal is (andEL (i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2 ∧ n ∈ Ī‰) ((1,0) = (i2,m2)) HcoordsR5).
We prove the intermediate claim HnOmega: n ∈ Ī‰.
An exact proof term for the current goal is (andER (i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2) (n ∈ Ī‰) HcoordsR4).
We prove the intermediate claim HcoordsR3: i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2.
An exact proof term for the current goal is (andEL (i2 ∈ 2 ∧ m2 ∈ Ī‰ ∧ j2 ∈ 2) (n ∈ Ī‰) HcoordsR4).
We prove the intermediate claim Hj2_2: j2 ∈ 2.
An exact proof term for the current goal is (andER (i2 ∈ 2 ∧ m2 ∈ Ī‰) (j2 ∈ 2) HcoordsR3).
We prove the intermediate claim HcoordsR2: i2 ∈ 2 ∧ m2 ∈ Ī‰.
An exact proof term for the current goal is (andEL (i2 ∈ 2 ∧ m2 ∈ Ī‰) (j2 ∈ 2) HcoordsR3).
We prove the intermediate claim Hi2Eq1: i2 = 1.
We will prove i2 = 1.
rewrite the current goal using (tuple_2_0_eq i2 m2) (from right to left) at position 1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left) at position 2.
We prove the intermediate claim Hproj0: (i2,m2) 0 = (1,0) 0.
rewrite the current goal using H10EqR (from right to left).
Use reflexivity.
An exact proof term for the current goal is Hproj0.
We prove the intermediate claim Hj2Eq1: j2 = 1.
Apply (HlexR (j2 = 1)) to the current goal.
Assume Hilj: i2 ∈ j2.
Apply FalseE to the current goal.
We prove the intermediate claim H1j: 1 ∈ j2.
rewrite the current goal using Hi2Eq1 (from right to left).
An exact proof term for the current goal is Hilj.
We prove the intermediate claim Hsub2: 2 ⊆ {0,1}.
An exact proof term for the current goal is Subq_2_UPair01.
We prove the intermediate claim Hj01: j2 ∈ {0,1}.
An exact proof term for the current goal is (Hsub2 j2 Hj2_2).
Apply (UPairE j2 0 1 Hj01 False) to the current goal.
Assume Hj0: j2 = 0.
We prove the intermediate claim H1in0: 1 ∈ 0.
rewrite the current goal using Hj0 (from right to left) at position 2.
An exact proof term for the current goal is H1j.
An exact proof term for the current goal is (EmptyE 1 H1in0).
Assume Hj1: j2 = 1.
We prove the intermediate claim H1in1: 1 ∈ 1.
rewrite the current goal using Hj1 (from right to left) at position 2.
An exact proof term for the current goal is H1j.
An exact proof term for the current goal is (In_irref 1 H1in1).
Assume Hind: i2 = j2 ∧ m2 ∈ n.
We will prove j2 = 1.
We prove the intermediate claim Hij: i2 = j2.
An exact proof term for the current goal is (andEL (i2 = j2) (m2 ∈ n) Hind).
rewrite the current goal using Hij (from right to left).
An exact proof term for the current goal is Hi2Eq1.
We prove the intermediate claim HbEq: b = (1,n).
We will prove b = (1,n).
rewrite the current goal using HbEq2 (from left to right).
rewrite the current goal using Hj2Eq1 (from left to right).
Use reflexivity.
We prove the intermediate claim HsuccOmega: ordsucc m ∈ Ī‰.
An exact proof term for the current goal is (omega_ordsucc m HmOmega).
We prove the intermediate claim H0sX: (0,ordsucc m) ∈ X.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 Ī‰ 0 (ordsucc m) In_0_2 HsuccOmega).
We prove the intermediate claim H0sL: order_rel X a (0,ordsucc m).
We will prove order_rel X a (0,ordsucc m).
rewrite the current goal using HXeq (from left to right) at position 1.
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_0k_0succk m HmOmega).
We prove the intermediate claim H0sR: order_rel X (0,ordsucc m) b.
We will prove order_rel X (0,ordsucc m) b.
rewrite the current goal using HXeq (from left to right) at position 1.
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_0k_1n (ordsucc m) n HsuccOmega HnOmega).
We prove the intermediate claim H0score: order_rel X a (0,ordsucc m) ∧ order_rel X (0,ordsucc m) b.
Apply andI to the current goal.
An exact proof term for the current goal is H0sL.
An exact proof term for the current goal is H0sR.
We prove the intermediate claim H0sinDef: (0,ordsucc m) ∈ {x ∈ X|order_rel X a x ∧ order_rel X x b}.
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) (0,ordsucc m) H0sX H0score).
We prove the intermediate claim H0sinU: (0,ordsucc m) ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is H0sinDef.
We prove the intermediate claim H0sEq10: (0,ordsucc m) = (1,0).
An exact proof term for the current goal is (SingE (1,0) (0,ordsucc m) H0sinU).
We prove the intermediate claim H0Eq1: 0 = 1.
We will prove 0 = 1.
rewrite the current goal using (tuple_2_0_eq 0 (ordsucc m)) (from right to left) at position 1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left) at position 2.
We prove the intermediate claim Hproj0: (0,ordsucc m) 0 = (1,0) 0.
rewrite the current goal using H0sEq10 (from left to right).
Use reflexivity.
An exact proof term for the current goal is Hproj0.
An exact proof term for the current goal is (neq_0_1 H0Eq1).
Assume HU2: U ∈ {I ∈ đ’Ģ X|∃b ∈ X, I = {x ∈ X|order_rel X x b}}.
We prove the intermediate claim Hexb: ∃b ∈ X, U = {x ∈ X|order_rel X x b}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b ∈ X, I0 = {x ∈ X|order_rel X x b}) U HU2).
Apply Hexb to the current goal.
Let b be given.
Assume HbPair.
Apply HbPair to the current goal.
Assume HbX: b ∈ X.
Assume HUeq: U = {x ∈ X|order_rel X x b}.
We prove the intermediate claim H10inU: (1,0) ∈ U.
An exact proof term for the current goal is (SingI (1,0)).
We prove the intermediate claim H10inDef: (1,0) ∈ {x ∈ X|order_rel X x b}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is H10inU.
We prove the intermediate claim Hrel: order_rel X (1,0) b.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X x0 b) (1,0) H10inDef).
We prove the intermediate claim HXeq: X = setprod 2 Ī‰.
Use reflexivity.
We prove the intermediate claim Hrel2: order_rel (setprod 2 Ī‰) (1,0) b.
We will prove order_rel (setprod 2 Ī‰) (1,0) b.
rewrite the current goal using HXeq (from right to left) at position 1.
An exact proof term for the current goal is Hrel.
We prove the intermediate claim Hex: ∃i m j n : set, i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i,m) ∧ b = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
An exact proof term for the current goal is (order_rel_setprod_2_omega_unfold (1,0) b Hrel2).
Apply Hex 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 Hcore.
We prove the intermediate claim Hcoords: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i,m) ∧ b = (j,n).
Apply Hcore to the current goal.
Assume Hcoords0 Hlex0.
An exact proof term for the current goal is Hcoords0.
We prove the intermediate claim Hlex: i ∈ j ∨ (i = j ∧ m ∈ n).
Apply Hcore to the current goal.
Assume Hcoords0 Hlex0.
An exact proof term for the current goal is Hlex0.
We prove the intermediate claim HbEq2: b = (j,n).
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i,m)) (b = (j,n)) Hcoords).
We prove the intermediate claim Hcoords5: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i,m).
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ (1,0) = (i,m)) (b = (j,n)) Hcoords).
We prove the intermediate claim H10Eq2: (1,0) = (i,m).
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰) ((1,0) = (i,m)) Hcoords5).
We prove the intermediate claim Hcoords4: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰) ((1,0) = (i,m)) Hcoords5).
We prove the intermediate claim HnOmega: n ∈ Ī‰.
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2) (n ∈ Ī‰) Hcoords4).
We prove the intermediate claim Hcoords3: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2) (n ∈ Ī‰) Hcoords4).
We prove the intermediate claim Hj2: j ∈ 2.
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰) (j ∈ 2) Hcoords3).
We prove the intermediate claim Hcoords2: i ∈ 2 ∧ m ∈ Ī‰.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰) (j ∈ 2) Hcoords3).
We prove the intermediate claim Hi2: i ∈ 2.
An exact proof term for the current goal is (andEL (i ∈ 2) (m ∈ Ī‰) Hcoords2).
We prove the intermediate claim HmOmega: m ∈ Ī‰.
An exact proof term for the current goal is (andER (i ∈ 2) (m ∈ Ī‰) Hcoords2).
We prove the intermediate claim HiEq: i = 1.
We will prove i = 1.
rewrite the current goal using (tuple_2_0_eq i m) (from right to left) at position 1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left) at position 2.
We prove the intermediate claim Hproj0: (i,m) 0 = (1,0) 0.
rewrite the current goal using H10Eq2 (from right to left).
Use reflexivity.
An exact proof term for the current goal is Hproj0.
We prove the intermediate claim Hj1: j = 1.
Apply (Hlex (j = 1)) to the current goal.
Assume Hilj: i ∈ j.
Apply FalseE to the current goal.
We prove the intermediate claim H1j: 1 ∈ j.
rewrite the current goal using HiEq (from right to left) at position 1.
An exact proof term for the current goal is Hilj.
We prove the intermediate claim Hsub2: 2 ⊆ {0,1}.
An exact proof term for the current goal is Subq_2_UPair01.
We prove the intermediate claim Hj01: j ∈ {0,1}.
An exact proof term for the current goal is (Hsub2 j Hj2).
Apply (UPairE j 0 1 Hj01 False) to the current goal.
Assume Hj0: j = 0.
We prove the intermediate claim H1in0: 1 ∈ 0.
rewrite the current goal using Hj0 (from right to left) at position 2.
An exact proof term for the current goal is H1j.
An exact proof term for the current goal is (EmptyE 1 H1in0).
Assume Hj1': j = 1.
We prove the intermediate claim H1in1: 1 ∈ 1.
rewrite the current goal using Hj1' (from right to left) at position 2.
An exact proof term for the current goal is H1j.
An exact proof term for the current goal is (In_irref 1 H1in1).
Assume Hind: i = j ∧ m ∈ n.
We will prove j = 1.
We prove the intermediate claim Hij: i = j.
An exact proof term for the current goal is (andEL (i = j) (m ∈ n) Hind).
rewrite the current goal using Hij (from right to left) at position 1.
An exact proof term for the current goal is HiEq.
We prove the intermediate claim HbEq: b = (1,n).
We will prove b = (1,n).
rewrite the current goal using Hj1 (from right to left) at position 2.
An exact proof term for the current goal is HbEq2.
We prove the intermediate claim H0omega: 0 ∈ Ī‰.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim H00X: (0,0) ∈ X.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 Ī‰ 0 0 In_0_2 H0omega).
We prove the intermediate claim H00rel: order_rel X (0,0) b.
We will prove order_rel X (0,0) b.
rewrite the current goal using HXeq (from left to right) at position 1.
rewrite the current goal using HbEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_00_1n n HnOmega).
We prove the intermediate claim H00inDef: (0,0) ∈ {x ∈ X|order_rel X x b}.
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b) (0,0) H00X H00rel).
We prove the intermediate claim H00inU: (0,0) ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is H00inDef.
We prove the intermediate claim H00Eq10: (0,0) = (1,0).
An exact proof term for the current goal is (SingE (1,0) (0,0) H00inU).
We prove the intermediate claim H0Eq1: 0 = 1.
We will prove 0 = 1.
rewrite the current goal using (tuple_2_0_eq 0 0) (from right to left) at position 1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left) at position 2.
We prove the intermediate claim Hproj0: (0,0) 0 = (1,0) 0.
rewrite the current goal using H00Eq10 (from left to right).
Use reflexivity.
An exact proof term for the current goal is Hproj0.
An exact proof term for the current goal is (neq_0_1 H0Eq1).
An exact proof term for the current goal is HU12.
Assume HU3: U ∈ {I ∈ đ’Ģ X|∃a ∈ X, I = {x ∈ X|order_rel X a x}}.
We prove the intermediate claim Hexa: ∃a ∈ X, U = {x ∈ X|order_rel X a x}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, I0 = {x ∈ X|order_rel X a x}) U HU3).
Apply Hexa to the current goal.
Let a be given.
Assume HaPair.
Apply HaPair to the current goal.
Assume HaX: a ∈ X.
Assume HUeq: U = {x ∈ X|order_rel X a x}.
We prove the intermediate claim H10inU: (1,0) ∈ U.
An exact proof term for the current goal is (SingI (1,0)).
We prove the intermediate claim H10inDef: (1,0) ∈ {x ∈ X|order_rel X a x}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is H10inU.
We prove the intermediate claim Hrel: order_rel X a (1,0).
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a x0) (1,0) H10inDef).
We prove the intermediate claim HXeq: X = setprod 2 Ī‰.
Use reflexivity.
We prove the intermediate claim Hrel2: order_rel (setprod 2 Ī‰) a (1,0).
We will prove order_rel (setprod 2 Ī‰) a (1,0).
rewrite the current goal using HXeq (from right to left) at position 1.
An exact proof term for the current goal is Hrel.
We prove the intermediate claim Hex: ∃i m j n : set, i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ a = (i,m) ∧ (1,0) = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n)).
An exact proof term for the current goal is (order_rel_setprod_2_omega_unfold a (1,0) Hrel2).
Apply Hex 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 Hcore.
We prove the intermediate claim Hcoords: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ a = (i,m) ∧ (1,0) = (j,n).
Apply Hcore to the current goal.
Assume Hcoords0 Hlex0.
An exact proof term for the current goal is Hcoords0.
We prove the intermediate claim Hlex: i ∈ j ∨ (i = j ∧ m ∈ n).
Apply Hcore to the current goal.
Assume Hcoords0 Hlex0.
An exact proof term for the current goal is Hlex0.
We prove the intermediate claim HjnEq: (1,0) = (j,n).
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ a = (i,m)) ((1,0) = (j,n)) Hcoords).
We prove the intermediate claim Hcoords5: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ a = (i,m).
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰ ∧ a = (i,m)) ((1,0) = (j,n)) Hcoords).
We prove the intermediate claim HaEq2: a = (i,m).
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰) (a = (i,m)) Hcoords5).
We prove the intermediate claim Hcoords4: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2 ∧ n ∈ Ī‰) (a = (i,m)) Hcoords5).
We prove the intermediate claim HnOmega: n ∈ Ī‰.
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2) (n ∈ Ī‰) Hcoords4).
We prove the intermediate claim Hcoords3: i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰ ∧ j ∈ 2) (n ∈ Ī‰) Hcoords4).
We prove the intermediate claim Hj2: j ∈ 2.
An exact proof term for the current goal is (andER (i ∈ 2 ∧ m ∈ Ī‰) (j ∈ 2) Hcoords3).
We prove the intermediate claim Hcoords2: i ∈ 2 ∧ m ∈ Ī‰.
An exact proof term for the current goal is (andEL (i ∈ 2 ∧ m ∈ Ī‰) (j ∈ 2) Hcoords3).
We prove the intermediate claim Hi2: i ∈ 2.
An exact proof term for the current goal is (andEL (i ∈ 2) (m ∈ Ī‰) Hcoords2).
We prove the intermediate claim HmOmega: m ∈ Ī‰.
An exact proof term for the current goal is (andER (i ∈ 2) (m ∈ Ī‰) Hcoords2).
We prove the intermediate claim HjEq1: j = 1.
We will prove j = 1.
rewrite the current goal using (tuple_2_0_eq j n) (from right to left) at position 1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left) at position 2.
We prove the intermediate claim Hproj0: (j,n) 0 = (1,0) 0.
rewrite the current goal using HjnEq (from right to left).
Use reflexivity.
An exact proof term for the current goal is Hproj0.
We prove the intermediate claim HnEq0: n = 0.
We will prove n = 0.
rewrite the current goal using (tuple_2_1_eq j n) (from right to left) at position 1.
rewrite the current goal using HjnEq (from right to left) at position 1.
An exact proof term for the current goal is (tuple_2_1_eq 1 0).
We prove the intermediate claim HiEq0: i = 0.
Apply (Hlex (i = 0)) to the current goal.
Assume Hilj: i ∈ j.
We will prove i = 0.
We prove the intermediate claim HiIn1: i ∈ 1.
rewrite the current goal using HjEq1 (from right to left).
An exact proof term for the current goal is Hilj.
We prove the intermediate claim HiInSing0: i ∈ {0}.
rewrite the current goal using eq_1_Sing0 (from right to left).
An exact proof term for the current goal is HiIn1.
An exact proof term for the current goal is (SingE 0 i HiInSing0).
Assume Hind: i = j ∧ m ∈ n.
Apply FalseE to the current goal.
We prove the intermediate claim Hmn: m ∈ n.
An exact proof term for the current goal is (andER (i = j) (m ∈ n) Hind).
We prove the intermediate claim HmIn0: m ∈ 0.
rewrite the current goal using HnEq0 (from right to left).
An exact proof term for the current goal is Hmn.
An exact proof term for the current goal is (EmptyE m HmIn0).
We prove the intermediate claim HaEq: a = (0,m).
We will prove a = (0,m).
rewrite the current goal using HaEq2 (from left to right).
rewrite the current goal using HiEq0 (from left to right).
Use reflexivity.
We prove the intermediate claim HsuccOmega: ordsucc m ∈ Ī‰.
An exact proof term for the current goal is (omega_ordsucc m HmOmega).
We prove the intermediate claim H0sX: (0,ordsucc m) ∈ X.
rewrite the current goal using HXeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 Ī‰ 0 (ordsucc m) In_0_2 HsuccOmega).
We prove the intermediate claim H0srel: order_rel X a (0,ordsucc m).
We will prove order_rel X a (0,ordsucc m).
rewrite the current goal using HXeq (from left to right) at position 1.
rewrite the current goal using HaEq (from left to right).
An exact proof term for the current goal is (order_rel_setprod_2_omega_0k_0succk m HmOmega).
We prove the intermediate claim H0sinDef: (0,ordsucc m) ∈ {x ∈ X|order_rel X a x}.
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a x0) (0,ordsucc m) H0sX H0srel).
We prove the intermediate claim H0sinU: (0,ordsucc m) ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is H0sinDef.
We prove the intermediate claim H0sEq10: (0,ordsucc m) = (1,0).
An exact proof term for the current goal is (SingE (1,0) (0,ordsucc m) H0sinU).
We prove the intermediate claim H0Eq1: 0 = 1.
We will prove 0 = 1.
rewrite the current goal using (tuple_2_0_eq 0 (ordsucc m)) (from right to left) at position 1.
rewrite the current goal using (tuple_2_0_eq 1 0) (from right to left) at position 2.
We prove the intermediate claim Hproj0: (0,ordsucc m) 0 = (1,0) 0.
rewrite the current goal using H0sEq10 (from left to right).
Use reflexivity.
An exact proof term for the current goal is Hproj0.
An exact proof term for the current goal is (neq_0_1 H0Eq1).
An exact proof term for the current goal is HUold.
∎