Let W be given.

Assume HW: W ∈ Fam2.

Apply (ReplE_impred Fam (λI : set ⇒ rectangle_set {a} I) W HW (W ∈ T)) to the current goal.

Let I be given.

Assume HIinFam Heq.

rewrite the current goal using Heq (from left to right).

We prove the intermediate claim HFamSubBq: Fam ⊆ Bq.

An exact proof term for the current goal is (PowerE Bq Fam HFamPow).

We prove the intermediate claim HIbq: I ∈ Bq.

An exact proof term for the current goal is (HFamSubBq I HIinFam).

Apply (famunionE_impred rational_numbers (λq1 : set ⇒ {open_interval q1 q2|q2 ∈ rational_numbers}) I HIbq (rectangle_set {a} I ∈ T)) to the current goal.

Let q1 be given.

Assume Hq1Q HIq1.

Apply (ReplE_impred rational_numbers (λq2 : set ⇒ open_interval q1 q2) I HIq1 (rectangle_set {a} I ∈ T)) to the current goal.

Let q2 be given.

Assume Hq2Q HIeq.

rewrite the current goal using HIeq (from left to right).

Set pL to be the term (a,q1).

Set pU to be the term (a,q2).

We prove the intermediate claim Hq1R: q1 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q1 Hq1Q).

We prove the intermediate claim Hq2R: q2 ∈ R.

An exact proof term for the current goal is (rational_numbers_in_R q2 Hq2Q).

We prove the intermediate claim HpLX0: pL ∈ X0.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R a q1 HaR Hq1R).

We prove the intermediate claim HpUX0: pU ∈ X0.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R a q2 HaR Hq2R).

Set U1 to be the term open_ray_upper X0 pL.

Set U2 to be the term open_ray_lower X0 pU.

We prove the intermediate claim HS: subbasis_on X0 (open_rays_subbasis X0).

An exact proof term for the current goal is (open_rays_subbasis_is_subbasis X0).

We prove the intermediate claim HU1S: U1 ∈ open_rays_subbasis X0.

An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis X0 pL HpLX0).

We prove the intermediate claim HU2S: U2 ∈ open_rays_subbasis X0.

An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis X0 pU HpUX0).

We prove the intermediate claim HdefT: T = generated_topology_from_subbasis X0 (open_rays_subbasis X0).

Use reflexivity.

We prove the intermediate claim HdefT2: generated_topology_from_subbasis X0 (open_rays_subbasis X0) = generated_topology X0 (basis_of_subbasis X0 (open_rays_subbasis X0)).

Use reflexivity.

We prove the intermediate claim HBsub: basis_on X0 (basis_of_subbasis X0 (open_rays_subbasis X0)).

An exact proof term for the current goal is (finite_intersections_basis_of_subbasis X0 (open_rays_subbasis X0) HS).

We prove the intermediate claim HU1T: U1 ∈ T.

Apply (xm (U1 = Empty)) to the current goal.

Assume HU1Empty.

rewrite the current goal using HU1Empty (from left to right).

An exact proof term for the current goal is (topology_has_empty X0 T HT).

Assume HU1ne: U1 ≠ Empty.

We prove the intermediate claim HU1B: U1 ∈ basis_of_subbasis X0 (open_rays_subbasis X0).

We prove the intermediate claim HU1F: U1 ∈ finite_intersections_of X0 (open_rays_subbasis X0).

We prove the intermediate claim HU1subX0: U1 ⊆ X0.

Let x be given.

Assume Hx: x ∈ U1.

An exact proof term for the current goal is (SepE1 X0 (λy : set ⇒ order_rel X0 pL y) x Hx).

We prove the intermediate claim Hintsing: intersection_of_family X0 {U1} = U1.

An exact proof term for the current goal is (intersection_of_family_singleton_eq X0 U1 HU1subX0).

We prove the intermediate claim HFsub: {U1} ∈ finite_subcollections (open_rays_subbasis X0).

We prove the intermediate claim HFpow: {U1} ∈ 𝒫 (open_rays_subbasis X0).

Apply PowerI to the current goal.

Let s be given.

Assume Hs: s ∈ {U1}.

We prove the intermediate claim Hseq: s = U1.

An exact proof term for the current goal is (SingE U1 s Hs).

rewrite the current goal using Hseq (from left to right).

An exact proof term for the current goal is HU1S.

We prove the intermediate claim HFfin: finite {U1}.

An exact proof term for the current goal is (Sing_finite U1).

An exact proof term for the current goal is (SepI (𝒫 (open_rays_subbasis X0)) (λF0 : set ⇒ finite F0) {U1} HFpow HFfin).

We prove the intermediate claim Hintsing_in: intersection_of_family X0 {U1} ∈ finite_intersections_of X0 (open_rays_subbasis X0).

An exact proof term for the current goal is (ReplI (finite_subcollections (open_rays_subbasis X0)) (λF0 : set ⇒ intersection_of_family X0 F0) {U1} HFsub).

rewrite the current goal using Hintsing (from right to left).

An exact proof term for the current goal is Hintsing_in.

An exact proof term for the current goal is (SepI (finite_intersections_of X0 (open_rays_subbasis X0)) (λb0 : set ⇒ b0 ≠ Empty) U1 HU1F HU1ne).

rewrite the current goal using HdefT (from left to right).

rewrite the current goal using HdefT2 (from left to right).

An exact proof term for the current goal is (generated_topology_contains_basis X0 (basis_of_subbasis X0 (open_rays_subbasis X0)) HBsub U1 HU1B).

We prove the intermediate claim HU2T: U2 ∈ T.

Apply (xm (U2 = Empty)) to the current goal.

Assume HU2Empty.

rewrite the current goal using HU2Empty (from left to right).

An exact proof term for the current goal is (topology_has_empty X0 T HT).

Assume HU2ne: U2 ≠ Empty.

We prove the intermediate claim HU2B: U2 ∈ basis_of_subbasis X0 (open_rays_subbasis X0).

We prove the intermediate claim HU2F: U2 ∈ finite_intersections_of X0 (open_rays_subbasis X0).

We prove the intermediate claim HU2subX0: U2 ⊆ X0.

Let x be given.

Assume Hx: x ∈ U2.

An exact proof term for the current goal is (SepE1 X0 (λy : set ⇒ order_rel X0 y pU) x Hx).

We prove the intermediate claim Hintsing: intersection_of_family X0 {U2} = U2.

An exact proof term for the current goal is (intersection_of_family_singleton_eq X0 U2 HU2subX0).

We prove the intermediate claim HFsub: {U2} ∈ finite_subcollections (open_rays_subbasis X0).

We prove the intermediate claim HFpow: {U2} ∈ 𝒫 (open_rays_subbasis X0).

Apply PowerI to the current goal.

Let s be given.

Assume Hs: s ∈ {U2}.

We prove the intermediate claim Hseq: s = U2.

An exact proof term for the current goal is (SingE U2 s Hs).

rewrite the current goal using Hseq (from left to right).

An exact proof term for the current goal is HU2S.

We prove the intermediate claim HFfin: finite {U2}.

An exact proof term for the current goal is (Sing_finite U2).

An exact proof term for the current goal is (SepI (𝒫 (open_rays_subbasis X0)) (λF0 : set ⇒ finite F0) {U2} HFpow HFfin).

We prove the intermediate claim Hintsing_in: intersection_of_family X0 {U2} ∈ finite_intersections_of X0 (open_rays_subbasis X0).

An exact proof term for the current goal is (ReplI (finite_subcollections (open_rays_subbasis X0)) (λF0 : set ⇒ intersection_of_family X0 F0) {U2} HFsub).

rewrite the current goal using Hintsing (from right to left).

An exact proof term for the current goal is Hintsing_in.

An exact proof term for the current goal is (SepI (finite_intersections_of X0 (open_rays_subbasis X0)) (λb0 : set ⇒ b0 ≠ Empty) U2 HU2F HU2ne).

rewrite the current goal using HdefT (from left to right).

rewrite the current goal using HdefT2 (from left to right).

An exact proof term for the current goal is (generated_topology_contains_basis X0 (basis_of_subbasis X0 (open_rays_subbasis X0)) HBsub U2 HU2B).

We prove the intermediate claim Hinter: U1 ∩ U2 ∈ T.

An exact proof term for the current goal is (topology_binintersect_closed X0 T U1 U2 HT HU1T HU2T).

We prove the intermediate claim HeqRect: rectangle_set {a} (open_interval q1 q2) = U1 ∩ U2.

Apply set_ext to the current goal.

Let p be given.

Assume Hp: p ∈ rectangle_set {a} (open_interval q1 q2).

We will prove p ∈ U1 ∩ U2.

We prove the intermediate claim HpS: p ∈ setprod {a} (open_interval q1 q2).

rewrite the current goal using rectangle_set_def (from right to left).

An exact proof term for the current goal is Hp.

We prove the intermediate claim Hp0Sing: p 0 ∈ {a}.

An exact proof term for the current goal is (ap0_Sigma {a} (λ_ : set ⇒ open_interval q1 q2) p HpS).

We prove the intermediate claim Hp0eq: p 0 = a.

An exact proof term for the current goal is (SingE a (p 0) Hp0Sing).

We prove the intermediate claim Hp1Int: p 1 ∈ open_interval q1 q2.

An exact proof term for the current goal is (ap1_Sigma {a} (λ_ : set ⇒ open_interval q1 q2) p HpS).

We prove the intermediate claim Hp1R: p 1 ∈ R.

An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) (p 1) Hp1Int).

We prove the intermediate claim Hp1ineq: Rlt q1 (p 1) ∧ Rlt (p 1) q2.

An exact proof term for the current goal is (SepE2 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) (p 1) Hp1Int).

We prove the intermediate claim HltL: Rlt q1 (p 1).

An exact proof term for the current goal is (andEL (Rlt q1 (p 1)) (Rlt (p 1) q2) Hp1ineq).

We prove the intermediate claim HltU: Rlt (p 1) q2.

An exact proof term for the current goal is (andER (Rlt q1 (p 1)) (Rlt (p 1) q2) Hp1ineq).

We prove the intermediate claim HsingSub: {a} ⊆ R.

An exact proof term for the current goal is (singleton_subset a R HaR).

We prove the intermediate claim HintSub: open_interval q1 q2 ⊆ R.

Let y be given.

Assume Hy: y ∈ open_interval q1 q2.

An exact proof term for the current goal is (SepE1 R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) y Hy).

We prove the intermediate claim HpX0: p ∈ X0.

An exact proof term for the current goal is ((setprod_Subq {a} (open_interval q1 q2) R R HsingSub HintSub) p Hp).

We prove the intermediate claim HpEta: p = (p 0,p 1).

An exact proof term for the current goal is (setprod_eta R R p HpX0).

We prove the intermediate claim HrelU1: order_rel X0 pL (p 0,p 1).

We prove the intermediate claim Hcore: a = p 0 ∧ Rlt q1 (p 1).

Apply andI to the current goal.

rewrite the current goal using Hp0eq (from right to left).

Use reflexivity.

An exact proof term for the current goal is HltL.

An exact proof term for the current goal is (order_rel_setprod_R_R_intro a q1 (p 0) (p 1) (orIR (Rlt a (p 0)) (a = (p 0) ∧ Rlt q1 (p 1)) Hcore)).

We prove the intermediate claim HrelU2: order_rel X0 (p 0,p 1) pU.

We prove the intermediate claim Hcore: (p 0) = a ∧ Rlt (p 1) q2.

Apply andI to the current goal.

rewrite the current goal using Hp0eq (from left to right).

Use reflexivity.

An exact proof term for the current goal is HltU.

An exact proof term for the current goal is (order_rel_setprod_R_R_intro (p 0) (p 1) a q2 (orIR (Rlt (p 0) a) ((p 0) = a ∧ Rlt (p 1) q2) Hcore)).

We prove the intermediate claim HpX0pair: (p 0,p 1) ∈ X0.

rewrite the current goal using HpEta (from right to left).

An exact proof term for the current goal is HpX0.

Apply binintersectI to the current goal.

rewrite the current goal using HpEta (from left to right).

An exact proof term for the current goal is (SepI X0 (λx0 : set ⇒ order_rel X0 pL x0) (p 0,p 1) HpX0pair HrelU1).

rewrite the current goal using HpEta (from left to right).

An exact proof term for the current goal is (SepI X0 (λx0 : set ⇒ order_rel X0 x0 pU) (p 0,p 1) HpX0pair HrelU2).

Let p be given.

Assume Hp: p ∈ U1 ∩ U2.

We will prove p ∈ rectangle_set {a} (open_interval q1 q2).

We prove the intermediate claim HpU1: p ∈ U1.

An exact proof term for the current goal is (binintersectE1 U1 U2 p Hp).

We prove the intermediate claim HpU2: p ∈ U2.

An exact proof term for the current goal is (binintersectE2 U1 U2 p Hp).

We prove the intermediate claim HpX0: p ∈ X0.

An exact proof term for the current goal is (SepE1 X0 (λx0 : set ⇒ order_rel X0 pL x0) p HpU1).

Set p0 to be the term p 0.

Set p1 to be the term p 1.

We prove the intermediate claim HpEta: p = (p0,p1).

An exact proof term for the current goal is (setprod_eta R R p HpX0).

We prove the intermediate claim Hrel1: order_rel X0 pL p.

An exact proof term for the current goal is (SepE2 X0 (λx0 : set ⇒ order_rel X0 pL x0) p HpU1).

We prove the intermediate claim Hrel2: order_rel X0 p pU.

An exact proof term for the current goal is (SepE2 X0 (λx0 : set ⇒ order_rel X0 x0 pU) p HpU2).

We prove the intermediate claim Hrel1': order_rel X0 pL (p0,p1).

rewrite the current goal using HpEta (from right to left) at position 1.

An exact proof term for the current goal is Hrel1.

We prove the intermediate claim Hrel2': order_rel X0 (p0,p1) pU.

rewrite the current goal using HpEta (from right to left) at position 1.

An exact proof term for the current goal is Hrel2.

We prove the intermediate claim Hex1: ∃a1 a2 b1 b2 : set, pL = (a1,a2) ∧ (p0,p1) = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).

An exact proof term for the current goal is (order_rel_setprod_R_R_unfold pL (p0,p1) Hrel1').

We prove the intermediate claim Hex2: ∃a1 a2 b1 b2 : set, (p0,p1) = (a1,a2) ∧ pU = (b1,b2) ∧ (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)).

An exact proof term for the current goal is (order_rel_setprod_R_R_unfold (p0,p1) pU Hrel2').

Apply Hex1 to the current goal.

Let a1 be given.

Assume Hc1.

Apply Hc1 to the current goal.

Let a2 be given.

Assume Hc2.

Apply Hc2 to the current goal.

Let b1 be given.

Assume Hd1.

Apply Hd1 to the current goal.

Let b2 be given.

Assume Hpack1.

We prove the intermediate claim Heq1: pL = (a1,a2) ∧ (p0,p1) = (b1,b2).

An exact proof term for the current goal is (andEL (pL = (a1,a2) ∧ (p0,p1) = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hpack1).

We prove the intermediate claim Hdisj1: Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2).

An exact proof term for the current goal is (andER (pL = (a1,a2) ∧ (p0,p1) = (b1,b2)) (Rlt a1 b1 ∨ (a1 = b1 ∧ Rlt a2 b2)) Hpack1).

We prove the intermediate claim HpLeq: pL = (a1,a2).

An exact proof term for the current goal is (andEL (pL = (a1,a2)) ((p0,p1) = (b1,b2)) Heq1).

We prove the intermediate claim HppEq: (p0,p1) = (b1,b2).

An exact proof term for the current goal is (andER (pL = (a1,a2)) ((p0,p1) = (b1,b2)) Heq1).

We prove the intermediate claim Ha1eq: a1 = a.

We prove the intermediate claim Ha1eq0: a = a1.

rewrite the current goal using (tuple_2_0_eq a q1) (from right to left).

rewrite the current goal using (tuple_2_0_eq a1 a2) (from right to left).

rewrite the current goal using HpLeq (from right to left).

Use reflexivity.

rewrite the current goal using Ha1eq0 (from left to right).

Use reflexivity.

We prove the intermediate claim Ha2eq: a2 = q1.

We prove the intermediate claim Ha2eq0: q1 = a2.

rewrite the current goal using (tuple_2_1_eq a q1) (from right to left).

rewrite the current goal using (tuple_2_1_eq a1 a2) (from right to left).

rewrite the current goal using HpLeq (from right to left).

Use reflexivity.

rewrite the current goal using Ha2eq0 (from left to right).

Use reflexivity.

We prove the intermediate claim Hb1eq: b1 = p0.

We prove the intermediate claim Hb1eq0: p0 = b1.

rewrite the current goal using (tuple_2_0_eq p0 p1) (from right to left).

rewrite the current goal using (tuple_2_0_eq b1 b2) (from right to left).

rewrite the current goal using HppEq (from left to right).

Use reflexivity.

rewrite the current goal using Hb1eq0 (from left to right).

Use reflexivity.

We prove the intermediate claim Hb2eq: b2 = p1.

We prove the intermediate claim Hb2eq0: p1 = b2.

rewrite the current goal using (tuple_2_1_eq p0 p1) (from right to left).

rewrite the current goal using (tuple_2_1_eq b1 b2) (from right to left).

rewrite the current goal using HppEq (from left to right).

Use reflexivity.

rewrite the current goal using Hb2eq0 (from left to right).

Use reflexivity.

We prove the intermediate claim Hcases1: Rlt a p0 ∨ (a = p0 ∧ Rlt q1 p1).

Apply Hdisj1 to the current goal.

Assume Hlt.

Apply orIL to the current goal.

rewrite the current goal using Ha1eq (from right to left) at position 1.

rewrite the current goal using Hb1eq (from right to left) at position 1.

An exact proof term for the current goal is Hlt.

Assume Hcore.

Apply orIR to the current goal.

Apply andI to the current goal.

rewrite the current goal using Ha1eq (from right to left) at position 1.

rewrite the current goal using Hb1eq (from right to left) at position 1.

An exact proof term for the current goal is (andEL (a1 = b1) (Rlt a2 b2) Hcore).

rewrite the current goal using Ha2eq (from right to left) at position 1.

rewrite the current goal using Hb2eq (from right to left) at position 1.

An exact proof term for the current goal is (andER (a1 = b1) (Rlt a2 b2) Hcore).

Apply Hex2 to the current goal.

Let c1 be given.

Assume Hc1'.

Apply Hc1' to the current goal.

Let c2 be given.

Assume Hc2'.

Apply Hc2' to the current goal.

Let d1 be given.

Assume Hd1'.

Apply Hd1' to the current goal.

Let d2 be given.

Assume Hpack2.

We prove the intermediate claim Heq2: (p0,p1) = (c1,c2) ∧ pU = (d1,d2).

An exact proof term for the current goal is (andEL ((p0,p1) = (c1,c2) ∧ pU = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpack2).

We prove the intermediate claim Hdisj2: Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2).

An exact proof term for the current goal is (andER ((p0,p1) = (c1,c2) ∧ pU = (d1,d2)) (Rlt c1 d1 ∨ (c1 = d1 ∧ Rlt c2 d2)) Hpack2).

We prove the intermediate claim HpcEq: (p0,p1) = (c1,c2).

An exact proof term for the current goal is (andEL ((p0,p1) = (c1,c2)) (pU = (d1,d2)) Heq2).

We prove the intermediate claim HpUeq: pU = (d1,d2).

An exact proof term for the current goal is (andER ((p0,p1) = (c1,c2)) (pU = (d1,d2)) Heq2).

We prove the intermediate claim Hc1eq: c1 = p0.

We prove the intermediate claim Hc1eq0: p0 = c1.

rewrite the current goal using (tuple_2_0_eq p0 p1) (from right to left).

rewrite the current goal using (tuple_2_0_eq c1 c2) (from right to left).

rewrite the current goal using HpcEq (from left to right).

Use reflexivity.

rewrite the current goal using Hc1eq0 (from left to right).

Use reflexivity.

We prove the intermediate claim Hc2eq: c2 = p1.

We prove the intermediate claim Hc2eq0: p1 = c2.

rewrite the current goal using (tuple_2_1_eq p0 p1) (from right to left).

rewrite the current goal using (tuple_2_1_eq c1 c2) (from right to left).

rewrite the current goal using HpcEq (from left to right).

Use reflexivity.

rewrite the current goal using Hc2eq0 (from left to right).

Use reflexivity.

We prove the intermediate claim Hd1eq: d1 = a.

We prove the intermediate claim Hd1eq0: a = d1.

rewrite the current goal using (tuple_2_0_eq a q2) (from right to left).

rewrite the current goal using (tuple_2_0_eq d1 d2) (from right to left).

rewrite the current goal using HpUeq (from right to left).

Use reflexivity.

rewrite the current goal using Hd1eq0 (from left to right).

Use reflexivity.

We prove the intermediate claim Hd2eq: d2 = q2.

We prove the intermediate claim Hd2eq0: q2 = d2.

rewrite the current goal using (tuple_2_1_eq a q2) (from right to left).

rewrite the current goal using (tuple_2_1_eq d1 d2) (from right to left).

rewrite the current goal using HpUeq (from right to left).

Use reflexivity.

rewrite the current goal using Hd2eq0 (from left to right).

Use reflexivity.

We prove the intermediate claim Hcases2: Rlt p0 a ∨ (p0 = a ∧ Rlt p1 q2).

Apply Hdisj2 to the current goal.

Assume Hlt.

Apply orIL to the current goal.

rewrite the current goal using Hc1eq (from right to left) at position 1.

rewrite the current goal using Hd1eq (from right to left) at position 1.

An exact proof term for the current goal is Hlt.

Assume Hcore.

Apply orIR to the current goal.

Apply andI to the current goal.

rewrite the current goal using Hc1eq (from right to left) at position 1.

rewrite the current goal using Hd1eq (from right to left) at position 1.

An exact proof term for the current goal is (andEL (c1 = d1) (Rlt c2 d2) Hcore).

rewrite the current goal using Hc2eq (from right to left) at position 1.

rewrite the current goal using Hd2eq (from right to left) at position 1.

An exact proof term for the current goal is (andER (c1 = d1) (Rlt c2 d2) Hcore).

We prove the intermediate claim Hp0eq: p0 = a.

Apply Hcases1 to the current goal.

Assume Hltap0.

Apply FalseE to the current goal.

Apply Hcases2 to the current goal.

Assume Hltp0a.

An exact proof term for the current goal is (not_Rlt_sym a p0 Hltap0 Hltp0a).

Assume Hcore.

We prove the intermediate claim Hp0a: p0 = a.

An exact proof term for the current goal is (andEL (p0 = a) (Rlt p1 q2) Hcore).

We prove the intermediate claim HltAA: Rlt a a.

rewrite the current goal using Hp0a (from right to left) at position 2.

An exact proof term for the current goal is Hltap0.

An exact proof term for the current goal is (not_Rlt_refl a HaR HltAA).

Assume Hcore.

We prove the intermediate claim Haeqp0: a = p0.

An exact proof term for the current goal is (andEL (a = p0) (Rlt q1 p1) Hcore).

Use symmetry.

An exact proof term for the current goal is Haeqp0.

We prove the intermediate claim Hltq1: Rlt q1 p1.

Apply Hcases1 to the current goal.

Assume Hltap0.

Apply FalseE to the current goal.

Apply Hcases2 to the current goal.

Assume Hltp0a.

An exact proof term for the current goal is (not_Rlt_sym a p0 Hltap0 Hltp0a).

Assume Hcore.

We prove the intermediate claim Hp0a: p0 = a.

An exact proof term for the current goal is (andEL (p0 = a) (Rlt p1 q2) Hcore).

We prove the intermediate claim HltAA: Rlt a a.

rewrite the current goal using Hp0a (from right to left) at position 2.

An exact proof term for the current goal is Hltap0.

An exact proof term for the current goal is (not_Rlt_refl a HaR HltAA).

Assume Hcore.

An exact proof term for the current goal is (andER (a = p0) (Rlt q1 p1) Hcore).

We prove the intermediate claim Hltq2: Rlt p1 q2.

Apply Hcases2 to the current goal.

Assume Hltp0a.

Apply FalseE to the current goal.

We prove the intermediate claim HltAA: Rlt a a.

rewrite the current goal using Hp0eq (from right to left) at position 1.

An exact proof term for the current goal is Hltp0a.

An exact proof term for the current goal is (not_Rlt_refl a HaR HltAA).

Assume Hcore.

An exact proof term for the current goal is (andER (p0 = a) (Rlt p1 q2) Hcore).

rewrite the current goal using rectangle_set_def (from left to right).

We prove the intermediate claim Hp0Sing: p0 ∈ {a}.

rewrite the current goal using Hp0eq (from right to left).

An exact proof term for the current goal is (SingI p0).

We prove the intermediate claim Hp1Int: p1 ∈ open_interval q1 q2.

We prove the intermediate claim Hconj: Rlt q1 p1 ∧ Rlt p1 q2.

Apply andI to the current goal.

An exact proof term for the current goal is Hltq1.

An exact proof term for the current goal is Hltq2.

An exact proof term for the current goal is (SepI R (λz : set ⇒ Rlt q1 z ∧ Rlt z q2) p1 (ap1_Sigma R (λ_ : set ⇒ R) p HpX0) Hconj).

rewrite the current goal using HpEta (from left to right).

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma {a} (open_interval q1 q2) p0 p1 Hp0Sing Hp1Int).

rewrite the current goal using HeqRect (from left to right).

An exact proof term for the current goal is Hinter.