Let K1, le1, K2 and le2 be given.
Assume HK1: directed_set K1 le1.
Assume HK2: directed_set K2 le2.
We will prove directed_set (setprod K1 K2) (setprod_le K1 le1 K2 le2).
We prove the intermediate claim HdirDef: directed_set (setprod K1 K2) (setprod_le K1 le1 K2 le2) = ((setprod K1 K2 ≠ Empty ∧ partial_order_on (setprod K1 K2) (setprod_le K1 le1 K2 le2)) ∧ ∀a b : set, a ∈ (setprod K1 K2) → b ∈ (setprod K1 K2) → ∃c : set, c ∈ (setprod K1 K2) ∧ (a,c) ∈ (setprod_le K1 le1 K2 le2) ∧ (b,c) ∈ (setprod_le K1 le1 K2 le2)).
Use reflexivity.
rewrite the current goal using HdirDef (from left to right).
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HK1ne: K1 ≠ Empty.
An exact proof term for the current goal is (directed_set_nonempty K1 le1 HK1).
We prove the intermediate claim HK2ne: K2 ≠ Empty.
An exact proof term for the current goal is (directed_set_nonempty K2 le2 HK2).
Apply (nonempty_has_element K1 HK1ne) to the current goal.
Let a1 be given.
Assume Ha1: a1 ∈ K1.
Apply (nonempty_has_element K2 HK2ne) to the current goal.
Let a2 be given.
Assume Ha2: a2 ∈ K2.
We will prove setprod K1 K2 ≠ Empty.
We prove the intermediate claim Hmem: (a1,a2) ∈ setprod K1 K2.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K1 K2 a1 a2 Ha1 Ha2).
An exact proof term for the current goal is (elem_implies_nonempty (setprod K1 K2) (a1,a2) Hmem).
We prove the intermediate claim HleDef: setprod_le K1 le1 K2 le2 = {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
Use reflexivity.
rewrite the current goal using HleDef (from left to right).
We prove the intermediate claim Hpo1: partial_order_on K1 le1.
An exact proof term for the current goal is (directed_set_partial_order K1 le1 HK1).
We prove the intermediate claim Hpo2: partial_order_on K2 le2.
An exact proof term for the current goal is (directed_set_partial_order K2 le2 HK2).
We will prove partial_order_on (setprod K1 K2) {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
We prove the intermediate claim HpoDef: partial_order_on (setprod K1 K2) {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)} = (relation_on {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)} (setprod K1 K2) ∧ (∀a : set, a ∈ (setprod K1 K2) → (a,a) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}) ∧ (∀a b : set, a ∈ (setprod K1 K2) → b ∈ (setprod K1 K2) → (a,b) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)} → (b,a) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)} → a = b) ∧ (∀a b c : set, a ∈ (setprod K1 K2) → b ∈ (setprod K1 K2) → c ∈ (setprod K1 K2) → (a,b) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)} → (b,c) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)} → (a,c) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)})).
Use reflexivity.
rewrite the current goal using HpoDef (from left to right).
Apply and4I to the current goal.
Let x and y be given.
Assume Hxy: (x,y) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
We will prove x ∈ setprod K1 K2 ∧ y ∈ setprod K1 K2.
We prove the intermediate claim HxyXY: (x,y) ∈ setprod (setprod K1 K2) (setprod K1 K2).
An exact proof term for the current goal is (SepE1 (setprod (setprod K1 K2) (setprod K1 K2)) (λq : set ⇒ (((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)) (x,y) Hxy).
We prove the intermediate claim Hx0: ((x,y) 0) ∈ setprod K1 K2.
An exact proof term for the current goal is (ap0_Sigma (setprod K1 K2) (λ_ : set ⇒ setprod K1 K2) (x,y) HxyXY).
We prove the intermediate claim Hy0: ((x,y) 1) ∈ setprod K1 K2.
An exact proof term for the current goal is (ap1_Sigma (setprod K1 K2) (λ_ : set ⇒ setprod K1 K2) (x,y) HxyXY).
Apply andI to the current goal.
rewrite the current goal using (tuple_2_0_eq x y) (from right to left).
An exact proof term for the current goal is Hx0.
rewrite the current goal using (tuple_2_1_eq x y) (from right to left).
An exact proof term for the current goal is Hy0.
Let x be given.
Assume Hx: x ∈ setprod K1 K2.
We will prove (x,x) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
Apply (SepI (setprod (setprod K1 K2) (setprod K1 K2)) (λq : set ⇒ (((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)) (x,x)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (setprod K1 K2) (setprod K1 K2) x x Hx Hx).
Apply andI to the current goal.
We prove the intermediate claim Hx0: (x 0) ∈ K1.
An exact proof term for the current goal is (ap0_Sigma K1 (λ_ : set ⇒ K2) x Hx).
We prove the intermediate claim Hrefl1: ((x 0),(x 0)) ∈ le1.
An exact proof term for the current goal is (partial_order_on_refl K1 le1 Hpo1 (x 0) Hx0).
We prove the intermediate claim Hq0: ((x,x) 0) 0 = (x 0).
rewrite the current goal using (tuple_2_0_eq x x) (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: ((x,x) 1) 0 = (x 0).
rewrite the current goal using (tuple_2_1_eq x x) (from left to right).
Use reflexivity.
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using Hq1 (from left to right).
An exact proof term for the current goal is Hrefl1.
We prove the intermediate claim Hx1: (x 1) ∈ K2.
An exact proof term for the current goal is (ap1_Sigma K1 (λ_ : set ⇒ K2) x Hx).
We prove the intermediate claim Hrefl2: ((x 1),(x 1)) ∈ le2.
An exact proof term for the current goal is (partial_order_on_refl K2 le2 Hpo2 (x 1) Hx1).
We prove the intermediate claim Hq0: ((x,x) 0) 1 = (x 1).
rewrite the current goal using (tuple_2_0_eq x x) (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: ((x,x) 1) 1 = (x 1).
rewrite the current goal using (tuple_2_1_eq x x) (from left to right).
Use reflexivity.
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using Hq1 (from left to right).
An exact proof term for the current goal is Hrefl2.
Let x and y be given.
Assume Hx: x ∈ setprod K1 K2.
Assume Hy: y ∈ setprod K1 K2.
Assume Hxy: (x,y) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
Assume Hyx: (y,x) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
We will prove x = y.
We prove the intermediate claim Hxy0: (x,y) ∈ setprod_le K1 le1 K2 le2.
rewrite the current goal using HleDef (from left to right).
An exact proof term for the current goal is Hxy.
We prove the intermediate claim Hyx0: (y,x) ∈ setprod_le K1 le1 K2 le2.
rewrite the current goal using HleDef (from left to right).
An exact proof term for the current goal is Hyx.
We prove the intermediate claim Hxyc: ((x 0,y 0) ∈ le1) ∧ ((x 1,y 1) ∈ le2).
An exact proof term for the current goal is (setprod_le_pred K1 le1 K2 le2 x y Hxy0).
We prove the intermediate claim Hyxc: ((y 0,x 0) ∈ le1) ∧ ((y 1,x 1) ∈ le2).
An exact proof term for the current goal is (setprod_le_pred K1 le1 K2 le2 y x Hyx0).
We prove the intermediate claim Hx0: (x 0) ∈ K1.
An exact proof term for the current goal is (ap0_Sigma K1 (λ_ : set ⇒ K2) x Hx).
We prove the intermediate claim Hx1: (x 1) ∈ K2.
An exact proof term for the current goal is (ap1_Sigma K1 (λ_ : set ⇒ K2) x Hx).
We prove the intermediate claim Hy0: (y 0) ∈ K1.
An exact proof term for the current goal is (ap0_Sigma K1 (λ_ : set ⇒ K2) y Hy).
We prove the intermediate claim Hy1: (y 1) ∈ K2.
An exact proof term for the current goal is (ap1_Sigma K1 (λ_ : set ⇒ K2) y Hy).
We prove the intermediate claim Heq0: (x 0) = (y 0).
An exact proof term for the current goal is (partial_order_on_antisym K1 le1 Hpo1 (x 0) (y 0) Hx0 Hy0 (andEL ((x 0,y 0) ∈ le1) ((x 1,y 1) ∈ le2) Hxyc) (andEL ((y 0,x 0) ∈ le1) ((y 1,x 1) ∈ le2) Hyxc)).
We prove the intermediate claim Heq1: (x 1) = (y 1).
An exact proof term for the current goal is (partial_order_on_antisym K2 le2 Hpo2 (x 1) (y 1) Hx1 Hy1 (andER ((x 0,y 0) ∈ le1) ((x 1,y 1) ∈ le2) Hxyc) (andER ((y 0,x 0) ∈ le1) ((y 1,x 1) ∈ le2) Hyxc)).
We prove the intermediate claim Hxeta: x = (x 0,x 1).
An exact proof term for the current goal is (setprod_eta K1 K2 x Hx).
We prove the intermediate claim Hyeta: y = (y 0,y 1).
An exact proof term for the current goal is (setprod_eta K1 K2 y Hy).
rewrite the current goal using Hxeta (from left to right).
rewrite the current goal using Hyeta (from left to right).
rewrite the current goal using Heq0 (from left to right).
rewrite the current goal using Heq1 (from left to right).
Use reflexivity.
Let x, y and z be given.
Assume Hx: x ∈ setprod K1 K2.
Assume Hy: y ∈ setprod K1 K2.
Assume Hz: z ∈ setprod K1 K2.
Assume Hxy: (x,y) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
Assume Hyz: (y,z) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
We will prove (x,z) ∈ {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
We prove the intermediate claim Hxy0: (x,y) ∈ setprod_le K1 le1 K2 le2.
rewrite the current goal using HleDef (from left to right).
An exact proof term for the current goal is Hxy.
We prove the intermediate claim Hyz0: (y,z) ∈ setprod_le K1 le1 K2 le2.
rewrite the current goal using HleDef (from left to right).
An exact proof term for the current goal is Hyz.
We prove the intermediate claim Hxyc: ((x 0,y 0) ∈ le1) ∧ ((x 1,y 1) ∈ le2).
An exact proof term for the current goal is (setprod_le_pred K1 le1 K2 le2 x y Hxy0).
We prove the intermediate claim Hyzc: ((y 0,z 0) ∈ le1) ∧ ((y 1,z 1) ∈ le2).
An exact proof term for the current goal is (setprod_le_pred K1 le1 K2 le2 y z Hyz0).
We prove the intermediate claim Hx0: (x 0) ∈ K1.
An exact proof term for the current goal is (ap0_Sigma K1 (λ_ : set ⇒ K2) x Hx).
We prove the intermediate claim Hy0: (y 0) ∈ K1.
An exact proof term for the current goal is (ap0_Sigma K1 (λ_ : set ⇒ K2) y Hy).
We prove the intermediate claim Hz0: (z 0) ∈ K1.
An exact proof term for the current goal is (ap0_Sigma K1 (λ_ : set ⇒ K2) z Hz).
We prove the intermediate claim Hx1: (x 1) ∈ K2.
An exact proof term for the current goal is (ap1_Sigma K1 (λ_ : set ⇒ K2) x Hx).
We prove the intermediate claim Hy1: (y 1) ∈ K2.
An exact proof term for the current goal is (ap1_Sigma K1 (λ_ : set ⇒ K2) y Hy).
We prove the intermediate claim Hz1: (z 1) ∈ K2.
An exact proof term for the current goal is (ap1_Sigma K1 (λ_ : set ⇒ K2) z Hz).
We prove the intermediate claim Hxz0: ((x 0,z 0) ∈ le1).
An exact proof term for the current goal is (partial_order_on_trans K1 le1 Hpo1 (x 0) (y 0) (z 0) Hx0 Hy0 Hz0 (andEL ((x 0,y 0) ∈ le1) ((x 1,y 1) ∈ le2) Hxyc) (andEL ((y 0,z 0) ∈ le1) ((y 1,z 1) ∈ le2) Hyzc)).
We prove the intermediate claim Hxz1: ((x 1,z 1) ∈ le2).
An exact proof term for the current goal is (partial_order_on_trans K2 le2 Hpo2 (x 1) (y 1) (z 1) Hx1 Hy1 Hz1 (andER ((x 0,y 0) ∈ le1) ((x 1,y 1) ∈ le2) Hxyc) (andER ((y 0,z 0) ∈ le1) ((y 1,z 1) ∈ le2) Hyzc)).
Apply (SepI (setprod (setprod K1 K2) (setprod K1 K2)) (λq : set ⇒ (((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)) (x,z)) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (setprod K1 K2) (setprod K1 K2) x z Hx Hz).
Apply andI to the current goal.
We prove the intermediate claim Hq0: ((x,z) 0) 0 = (x 0).
rewrite the current goal using (tuple_2_0_eq x z) (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: ((x,z) 1) 0 = (z 0).
rewrite the current goal using (tuple_2_1_eq x z) (from left to right).
Use reflexivity.
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using Hq1 (from left to right).
An exact proof term for the current goal is Hxz0.
We prove the intermediate claim Hq0: ((x,z) 0) 1 = (x 1).
rewrite the current goal using (tuple_2_0_eq x z) (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: ((x,z) 1) 1 = (z 1).
rewrite the current goal using (tuple_2_1_eq x z) (from left to right).
Use reflexivity.
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using Hq1 (from left to right).
An exact proof term for the current goal is Hxz1.
Let a and b be given.
Assume Ha: a ∈ setprod K1 K2.
Assume Hb: b ∈ setprod K1 K2.
We prove the intermediate claim Ha1: (a 0) ∈ K1.
An exact proof term for the current goal is (ap0_Sigma K1 (λ_ : set ⇒ K2) a Ha).
We prove the intermediate claim Ha2: (a 1) ∈ K2.
An exact proof term for the current goal is (ap1_Sigma K1 (λ_ : set ⇒ K2) a Ha).
We prove the intermediate claim Hb1: (b 0) ∈ K1.
An exact proof term for the current goal is (ap0_Sigma K1 (λ_ : set ⇒ K2) b Hb).
We prove the intermediate claim Hb2: (b 1) ∈ K2.
An exact proof term for the current goal is (ap1_Sigma K1 (λ_ : set ⇒ K2) b Hb).
Apply (directed_set_upper_bound_property K1 le1 HK1 (a 0) (b 0) Ha1 Hb1) to the current goal.
Let c1 be given.
Assume Hc1: c1 ∈ K1 ∧ ((a 0),c1) ∈ le1 ∧ ((b 0),c1) ∈ le1.
We prove the intermediate claim Hc1mem: c1 ∈ K1.
Apply (and3E (c1 ∈ K1) (((a 0),c1) ∈ le1) (((b 0),c1) ∈ le1) Hc1 (c1 ∈ K1)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H1.
We prove the intermediate claim Hac1: ((a 0),c1) ∈ le1.
Apply (and3E (c1 ∈ K1) (((a 0),c1) ∈ le1) (((b 0),c1) ∈ le1) Hc1 (((a 0),c1) ∈ le1)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H2.
We prove the intermediate claim Hbc1: ((b 0),c1) ∈ le1.
Apply (and3E (c1 ∈ K1) (((a 0),c1) ∈ le1) (((b 0),c1) ∈ le1) Hc1 (((b 0),c1) ∈ le1)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H3.
Apply (directed_set_upper_bound_property K2 le2 HK2 (a 1) (b 1) Ha2 Hb2) to the current goal.
Let c2 be given.
Assume Hc2: c2 ∈ K2 ∧ ((a 1),c2) ∈ le2 ∧ ((b 1),c2) ∈ le2.
We prove the intermediate claim Hc2mem: c2 ∈ K2.
Apply (and3E (c2 ∈ K2) (((a 1),c2) ∈ le2) (((b 1),c2) ∈ le2) Hc2 (c2 ∈ K2)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H1.
We prove the intermediate claim Hac2: ((a 1),c2) ∈ le2.
Apply (and3E (c2 ∈ K2) (((a 1),c2) ∈ le2) (((b 1),c2) ∈ le2) Hc2 (((a 1),c2) ∈ le2)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H2.
We prove the intermediate claim Hbc2: ((b 1),c2) ∈ le2.
Apply (and3E (c2 ∈ K2) (((a 1),c2) ∈ le2) (((b 1),c2) ∈ le2) Hc2 (((b 1),c2) ∈ le2)) to the current goal.
Assume H1 H2 H3.
An exact proof term for the current goal is H3.
We use (c1,c2) to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma K1 K2 c1 c2 Hc1mem Hc2mem).
We prove the intermediate claim HleDef: setprod_le K1 le1 K2 le2 = {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
Use reflexivity.
rewrite the current goal using HleDef (from left to right).
Apply (SepI (setprod (setprod K1 K2) (setprod K1 K2)) (λq : set ⇒ (((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)) (a,(c1,c2))) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (setprod K1 K2) (setprod K1 K2) a (c1,c2) Ha (tuple_2_setprod_by_pair_Sigma K1 K2 c1 c2 Hc1mem Hc2mem)).
Apply andI to the current goal.
We prove the intermediate claim Hq0: ((a,(c1,c2)) 0) 0 = (a 0).
rewrite the current goal using (tuple_2_0_eq a (c1,c2)) (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: ((a,(c1,c2)) 1) 0 = ((c1,c2) 0).
rewrite the current goal using (tuple_2_1_eq a (c1,c2)) (from left to right).
Use reflexivity.
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using Hq1 (from left to right).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from left to right).
An exact proof term for the current goal is Hac1.
We prove the intermediate claim Hq0: ((a,(c1,c2)) 0) 1 = (a 1).
rewrite the current goal using (tuple_2_0_eq a (c1,c2)) (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: ((a,(c1,c2)) 1) 1 = ((c1,c2) 1).
rewrite the current goal using (tuple_2_1_eq a (c1,c2)) (from left to right).
Use reflexivity.
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using Hq1 (from left to right).
rewrite the current goal using (tuple_2_1_eq c1 c2) (from left to right).
An exact proof term for the current goal is Hac2.
We prove the intermediate claim HleDef: setprod_le K1 le1 K2 le2 = {q ∈ setprod (setprod K1 K2) (setprod K1 K2)|(((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)}.
Use reflexivity.
rewrite the current goal using HleDef (from left to right).
Apply (SepI (setprod (setprod K1 K2) (setprod K1 K2)) (λq : set ⇒ (((q 0) 0,(q 1) 0) ∈ le1) ∧ (((q 0) 1,(q 1) 1) ∈ le2)) (b,(c1,c2))) to the current goal.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (setprod K1 K2) (setprod K1 K2) b (c1,c2) Hb (tuple_2_setprod_by_pair_Sigma K1 K2 c1 c2 Hc1mem Hc2mem)).
Apply andI to the current goal.
We prove the intermediate claim Hq0: ((b,(c1,c2)) 0) 0 = (b 0).
rewrite the current goal using (tuple_2_0_eq b (c1,c2)) (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: ((b,(c1,c2)) 1) 0 = ((c1,c2) 0).
rewrite the current goal using (tuple_2_1_eq b (c1,c2)) (from left to right).
Use reflexivity.
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using Hq1 (from left to right).
rewrite the current goal using (tuple_2_0_eq c1 c2) (from left to right).
An exact proof term for the current goal is Hbc1.
We prove the intermediate claim Hq0: ((b,(c1,c2)) 0) 1 = (b 1).
rewrite the current goal using (tuple_2_0_eq b (c1,c2)) (from left to right).
Use reflexivity.
We prove the intermediate claim Hq1: ((b,(c1,c2)) 1) 1 = ((c1,c2) 1).
rewrite the current goal using (tuple_2_1_eq b (c1,c2)) (from left to right).
Use reflexivity.
rewrite the current goal using Hq0 (from left to right).
rewrite the current goal using Hq1 (from left to right).
rewrite the current goal using (tuple_2_1_eq c1 c2) (from left to right).
An exact proof term for the current goal is Hbc2.
∎