We will prove basis_on R (R_standard_basis ∪ R_K_basis).
We will prove (R_standard_basis ∪ R_K_basis) ⊆ 𝒫 R ∧ (∀x ∈ R, ∃b ∈ (R_standard_basis ∪ R_K_basis), x ∈ b) ∧ (∀b1 ∈ (R_standard_basis ∪ R_K_basis), ∀b2 ∈ (R_standard_basis ∪ R_K_basis), ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ (R_standard_basis ∪ R_K_basis), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
Apply and3I to the current goal.
Let U be given.
Assume HU: U ∈ (R_standard_basis ∪ R_K_basis).
Apply (binunionE' R_standard_basis R_K_basis U (U ∈ 𝒫 R)) to the current goal.
Assume HUstd: U ∈ R_standard_basis.
We prove the intermediate claim HUsubR: U ⊆ R.
An exact proof term for the current goal is (basis_elem_subset R R_standard_basis U R_standard_basis_is_basis_local HUstd).
An exact proof term for the current goal is (PowerI R U HUsubR).
Assume HUk: U ∈ R_K_basis.
We prove the intermediate claim Hexa: ∃a ∈ R, U ∈ {open_interval a b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) U HUk).
Apply Hexa to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (U ∈ {open_interval a b ∖ K_set|b ∈ R}) Hapair).
We prove the intermediate claim HUfam: U ∈ {open_interval a b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (andER (a ∈ R) (U ∈ {open_interval a b ∖ K_set|b ∈ R}) Hapair).
We prove the intermediate claim Hexb: ∃b ∈ R, U = open_interval a b ∖ K_set.
An exact proof term for the current goal is (ReplE R (λb0 : set ⇒ open_interval a b0 ∖ K_set) U HUfam).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate claim HbR: b ∈ R.
An exact proof term for the current goal is (andEL (b ∈ R) (U = open_interval a b ∖ K_set) Hbpair).
We prove the intermediate claim HUeq: U = open_interval a b ∖ K_set.
An exact proof term for the current goal is (andER (b ∈ R) (U = open_interval a b ∖ K_set) Hbpair).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim Hsub1: (open_interval a b ∖ K_set) ⊆ open_interval a b.
An exact proof term for the current goal is (setminus_Subq (open_interval a b) K_set).
We prove the intermediate claim Hsub2: open_interval a b ⊆ R.
An exact proof term for the current goal is (open_interval_Subq_R a b).
An exact proof term for the current goal is (PowerI R (open_interval a b ∖ K_set) (Subq_tra (open_interval a b ∖ K_set) (open_interval a b) R Hsub1 Hsub2)).
An exact proof term for the current goal is HU.
Let x be given.
Assume HxR: x ∈ R.
We prove the intermediate claim Hcov: ∀x0 ∈ R, ∃b ∈ R_standard_basis, x0 ∈ b.
An exact proof term for the current goal is (andER (R_standard_basis ⊆ 𝒫 R) (∀x0 ∈ R, ∃b ∈ R_standard_basis, x0 ∈ b) (andEL (R_standard_basis ⊆ 𝒫 R ∧ (∀x0 ∈ R, ∃b ∈ R_standard_basis, x0 ∈ b)) (∀b1 ∈ R_standard_basis, ∀b2 ∈ R_standard_basis, ∀x0 : set, x0 ∈ b1 → x0 ∈ b2 → ∃b3 ∈ R_standard_basis, x0 ∈ b3 ∧ b3 ⊆ b1 ∩ b2) R_standard_basis_is_basis_local)).
We prove the intermediate claim Hex: ∃b ∈ R_standard_basis, x ∈ b.
An exact proof term for the current goal is (Hcov x HxR).
Apply Hex to the current goal.
Let b be given.
Assume Hbpair.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 R_standard_basis R_K_basis b (andEL (b ∈ R_standard_basis) (x ∈ b) Hbpair)).
An exact proof term for the current goal is (andER (b ∈ R_standard_basis) (x ∈ b) Hbpair).
Let b1 be given.
Assume Hb1.
Let b2 be given.
Assume Hb2.
Let x be given.
Assume Hx1 Hx2.
We will prove ∃b3 ∈ (R_standard_basis ∪ R_K_basis), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
We prove the intermediate claim HstdInt: ∀u1 ∈ R_standard_basis, ∀u2 ∈ R_standard_basis, ∀x0 : set, x0 ∈ u1 → x0 ∈ u2 → ∃u3 ∈ R_standard_basis, x0 ∈ u3 ∧ u3 ⊆ u1 ∩ u2.
An exact proof term for the current goal is (andER (R_standard_basis ⊆ 𝒫 R ∧ (∀x0 ∈ R, ∃b ∈ R_standard_basis, x0 ∈ b)) (∀u1 ∈ R_standard_basis, ∀u2 ∈ R_standard_basis, ∀x0 : set, x0 ∈ u1 → x0 ∈ u2 → ∃u3 ∈ R_standard_basis, x0 ∈ u3 ∧ u3 ⊆ u1 ∩ u2) R_standard_basis_is_basis_local).
Apply (binunionE' R_standard_basis R_K_basis b1 (∃b3 ∈ (R_standard_basis ∪ R_K_basis), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb1Std: b1 ∈ R_standard_basis.
Apply (binunionE' R_standard_basis R_K_basis b2 (∃b3 ∈ (R_standard_basis ∪ R_K_basis), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb2Std: b2 ∈ R_standard_basis.
Apply (HstdInt b1 Hb1Std b2 Hb2Std x Hx1 Hx2) to the current goal.
Let b3std be given.
Assume Hb3pair.
We use b3std to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 R_standard_basis R_K_basis b3std (andEL (b3std ∈ R_standard_basis) (x ∈ b3std ∧ b3std ⊆ b1 ∩ b2) Hb3pair)).
An exact proof term for the current goal is (andER (b3std ∈ R_standard_basis) (x ∈ b3std ∧ b3std ⊆ b1 ∩ b2) Hb3pair).
Assume Hb2K: b2 ∈ R_K_basis.
We prove the intermediate claim Hexa2: ∃a2 ∈ R, b2 ∈ {open_interval a2 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) b2 Hb2K).
Apply Hexa2 to the current goal.
Let a2 be given.
Assume Ha2pair.
We prove the intermediate claim Ha2R: a2 ∈ R.
An exact proof term for the current goal is (andEL (a2 ∈ R) (b2 ∈ {open_interval a2 b ∖ K_set|b ∈ R}) Ha2pair).
We prove the intermediate claim Hb2fam: b2 ∈ {open_interval a2 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (andER (a2 ∈ R) (b2 ∈ {open_interval a2 b ∖ K_set|b ∈ R}) Ha2pair).
We prove the intermediate claim Hexb2: ∃bb2 ∈ R, b2 = open_interval a2 bb2 ∖ K_set.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ open_interval a2 bb ∖ K_set) b2 Hb2fam).
Apply Hexb2 to the current goal.
Let bb2 be given.
Assume Hbb2pair.
We prove the intermediate claim Hbb2R: bb2 ∈ R.
An exact proof term for the current goal is (andEL (bb2 ∈ R) (b2 = open_interval a2 bb2 ∖ K_set) Hbb2pair).
We prove the intermediate claim Hb2eq: b2 = open_interval a2 bb2 ∖ K_set.
An exact proof term for the current goal is (andER (bb2 ∈ R) (b2 = open_interval a2 bb2 ∖ K_set) Hbb2pair).
Set I2 to be the term open_interval a2 bb2.
We prove the intermediate claim HI2Std: I2 ∈ R_standard_basis.
We prove the intermediate claim HI2fam: I2 ∈ {open_interval a2 b|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval a2 b0) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) a2 I2 Ha2R HI2fam).
We prove the intermediate claim HxInB2: x ∈ I2 ∖ K_set.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim HxInI2: x ∈ I2.
An exact proof term for the current goal is (setminusE1 I2 K_set x HxInB2).
We prove the intermediate claim HxNotK: x ∉ K_set.
An exact proof term for the current goal is (setminusE2 I2 K_set x HxInB2).
Apply (HstdInt b1 Hb1Std I2 HI2Std x Hx1 HxInI2) to the current goal.
Let I0 be given.
Assume HI0pair.
We prove the intermediate claim HI0Std: I0 ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (I0 ∈ R_standard_basis) (x ∈ I0 ∧ I0 ⊆ b1 ∩ I2) HI0pair).
We prove the intermediate claim HI0rest: x ∈ I0 ∧ I0 ⊆ b1 ∩ I2.
An exact proof term for the current goal is (andER (I0 ∈ R_standard_basis) (x ∈ I0 ∧ I0 ⊆ b1 ∩ I2) HI0pair).
We prove the intermediate claim HxI0: x ∈ I0.
An exact proof term for the current goal is (andEL (x ∈ I0) (I0 ⊆ b1 ∩ I2) HI0rest).
We prove the intermediate claim HI0sub: I0 ⊆ b1 ∩ I2.
An exact proof term for the current goal is (andER (x ∈ I0) (I0 ⊆ b1 ∩ I2) HI0rest).
We prove the intermediate claim Hexc: ∃c ∈ R, I0 ∈ {open_interval c b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λc0 : set ⇒ {open_interval c0 b|b ∈ R}) I0 HI0Std).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpair.
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (I0 ∈ {open_interval c b|b ∈ R}) Hcpair).
We prove the intermediate claim HI0fam: I0 ∈ {open_interval c b|b ∈ R}.
An exact proof term for the current goal is (andER (c ∈ R) (I0 ∈ {open_interval c b|b ∈ R}) Hcpair).
We prove the intermediate claim Hexd: ∃d ∈ R, I0 = open_interval c d.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ open_interval c d0) I0 HI0fam).
Apply Hexd to the current goal.
Let d be given.
Assume Hdpair.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (I0 = open_interval c d) Hdpair).
We prove the intermediate claim HI0eq: I0 = open_interval c d.
An exact proof term for the current goal is (andER (d ∈ R) (I0 = open_interval c d) Hdpair).
Set Kint to be the term open_interval c d ∖ K_set.
We use Kint to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HKfam: Kint ∈ {open_interval c b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval c b0 ∖ K_set) d HdR).
We prove the intermediate claim HKinK: Kint ∈ R_K_basis.
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) c Kint HcR HKfam).
An exact proof term for the current goal is (binunionI2 R_standard_basis R_K_basis Kint HKinK).
Apply andI to the current goal.
We will prove x ∈ open_interval c d ∖ K_set.
Apply setminusI to the current goal.
We will prove x ∈ open_interval c d.
rewrite the current goal using HI0eq (from right to left).
An exact proof term for the current goal is HxI0.
An exact proof term for the current goal is HxNotK.
Let y be given.
Assume Hy: y ∈ Kint.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyOpen: y ∈ open_interval c d.
An exact proof term for the current goal is (setminusE1 (open_interval c d) K_set y Hy).
We prove the intermediate claim HyI0: y ∈ I0.
rewrite the current goal using HI0eq (from left to right).
An exact proof term for the current goal is HyOpen.
We prove the intermediate claim HyNotK: y ∉ K_set.
An exact proof term for the current goal is (setminusE2 (open_interval c d) K_set y Hy).
We prove the intermediate claim Hyb1I2: y ∈ b1 ∩ I2.
An exact proof term for the current goal is (HI0sub y HyI0).
We prove the intermediate claim Hyb1: y ∈ b1.
An exact proof term for the current goal is (binintersectE1 b1 I2 y Hyb1I2).
We prove the intermediate claim HyI2: y ∈ I2.
An exact proof term for the current goal is (binintersectE2 b1 I2 y Hyb1I2).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (setminusI I2 K_set y HyI2 HyNotK).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
An exact proof term for the current goal is Hb2.
Assume Hb1K: b1 ∈ R_K_basis.
Apply (binunionE' R_standard_basis R_K_basis b2 (∃b3 ∈ (R_standard_basis ∪ R_K_basis), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb2Std: b2 ∈ R_standard_basis.
We prove the intermediate claim Hexa1: ∃a1 ∈ R, b1 ∈ {open_interval a1 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) b1 Hb1K).
Apply Hexa1 to the current goal.
Let a1 be given.
Assume Ha1pair.
We prove the intermediate claim Ha1R: a1 ∈ R.
An exact proof term for the current goal is (andEL (a1 ∈ R) (b1 ∈ {open_interval a1 b ∖ K_set|b ∈ R}) Ha1pair).
We prove the intermediate claim Hb1fam: b1 ∈ {open_interval a1 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (andER (a1 ∈ R) (b1 ∈ {open_interval a1 b ∖ K_set|b ∈ R}) Ha1pair).
We prove the intermediate claim Hexb1: ∃bb1 ∈ R, b1 = open_interval a1 bb1 ∖ K_set.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ open_interval a1 bb ∖ K_set) b1 Hb1fam).
Apply Hexb1 to the current goal.
Let bb1 be given.
Assume Hbb1pair.
We prove the intermediate claim Hbb1R: bb1 ∈ R.
An exact proof term for the current goal is (andEL (bb1 ∈ R) (b1 = open_interval a1 bb1 ∖ K_set) Hbb1pair).
We prove the intermediate claim Hb1eq: b1 = open_interval a1 bb1 ∖ K_set.
An exact proof term for the current goal is (andER (bb1 ∈ R) (b1 = open_interval a1 bb1 ∖ K_set) Hbb1pair).
Set I1 to be the term open_interval a1 bb1.
We prove the intermediate claim HI1Std: I1 ∈ R_standard_basis.
We prove the intermediate claim HI1fam: I1 ∈ {open_interval a1 b|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval a1 b0) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) a1 I1 Ha1R HI1fam).
We prove the intermediate claim HxInB1: x ∈ I1 ∖ K_set.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxInI1: x ∈ I1.
An exact proof term for the current goal is (setminusE1 I1 K_set x HxInB1).
We prove the intermediate claim HxNotK: x ∉ K_set.
An exact proof term for the current goal is (setminusE2 I1 K_set x HxInB1).
Apply (HstdInt I1 HI1Std b2 Hb2Std x HxInI1 Hx2) to the current goal.
Let I0 be given.
Assume HI0pair.
We prove the intermediate claim HI0Std: I0 ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (I0 ∈ R_standard_basis) (x ∈ I0 ∧ I0 ⊆ I1 ∩ b2) HI0pair).
We prove the intermediate claim HI0rest: x ∈ I0 ∧ I0 ⊆ I1 ∩ b2.
An exact proof term for the current goal is (andER (I0 ∈ R_standard_basis) (x ∈ I0 ∧ I0 ⊆ I1 ∩ b2) HI0pair).
We prove the intermediate claim HxI0: x ∈ I0.
An exact proof term for the current goal is (andEL (x ∈ I0) (I0 ⊆ I1 ∩ b2) HI0rest).
We prove the intermediate claim HI0sub: I0 ⊆ I1 ∩ b2.
An exact proof term for the current goal is (andER (x ∈ I0) (I0 ⊆ I1 ∩ b2) HI0rest).
We prove the intermediate claim Hexc: ∃c ∈ R, I0 ∈ {open_interval c b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λc0 : set ⇒ {open_interval c0 b|b ∈ R}) I0 HI0Std).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpair.
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (I0 ∈ {open_interval c b|b ∈ R}) Hcpair).
We prove the intermediate claim HI0fam: I0 ∈ {open_interval c b|b ∈ R}.
An exact proof term for the current goal is (andER (c ∈ R) (I0 ∈ {open_interval c b|b ∈ R}) Hcpair).
We prove the intermediate claim Hexd: ∃d ∈ R, I0 = open_interval c d.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ open_interval c d0) I0 HI0fam).
Apply Hexd to the current goal.
Let d be given.
Assume Hdpair.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (I0 = open_interval c d) Hdpair).
We prove the intermediate claim HI0eq: I0 = open_interval c d.
An exact proof term for the current goal is (andER (d ∈ R) (I0 = open_interval c d) Hdpair).
Set Kint to be the term open_interval c d ∖ K_set.
We use Kint to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HKfam: Kint ∈ {open_interval c b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval c b0 ∖ K_set) d HdR).
We prove the intermediate claim HKinK: Kint ∈ R_K_basis.
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) c Kint HcR HKfam).
An exact proof term for the current goal is (binunionI2 R_standard_basis R_K_basis Kint HKinK).
Apply andI to the current goal.
We will prove x ∈ open_interval c d ∖ K_set.
Apply setminusI to the current goal.
We will prove x ∈ open_interval c d.
rewrite the current goal using HI0eq (from right to left).
An exact proof term for the current goal is HxI0.
An exact proof term for the current goal is HxNotK.
Let y be given.
Assume Hy: y ∈ Kint.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyOpen: y ∈ open_interval c d.
An exact proof term for the current goal is (setminusE1 (open_interval c d) K_set y Hy).
We prove the intermediate claim HyI0: y ∈ I0.
rewrite the current goal using HI0eq (from left to right).
An exact proof term for the current goal is HyOpen.
We prove the intermediate claim HyNotK: y ∉ K_set.
An exact proof term for the current goal is (setminusE2 (open_interval c d) K_set y Hy).
We prove the intermediate claim HyI1b2: y ∈ I1 ∩ b2.
An exact proof term for the current goal is (HI0sub y HyI0).
We prove the intermediate claim HyI1: y ∈ I1.
An exact proof term for the current goal is (binintersectE1 I1 b2 y HyI1b2).
We prove the intermediate claim Hyb2: y ∈ b2.
An exact proof term for the current goal is (binintersectE2 I1 b2 y HyI1b2).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (setminusI I1 K_set y HyI1 HyNotK).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2K: b2 ∈ R_K_basis.
We prove the intermediate claim Hexa1: ∃a1 ∈ R, b1 ∈ {open_interval a1 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) b1 Hb1K).
We prove the intermediate claim Hexa2: ∃a2 ∈ R, b2 ∈ {open_interval a2 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) b2 Hb2K).
Apply Hexa1 to the current goal.
Let a1 be given.
Assume Ha1pair.
We prove the intermediate claim Ha1R: a1 ∈ R.
An exact proof term for the current goal is (andEL (a1 ∈ R) (b1 ∈ {open_interval a1 b ∖ K_set|b ∈ R}) Ha1pair).
We prove the intermediate claim Hb1fam: b1 ∈ {open_interval a1 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (andER (a1 ∈ R) (b1 ∈ {open_interval a1 b ∖ K_set|b ∈ R}) Ha1pair).
We prove the intermediate claim Hexb1: ∃bb1 ∈ R, b1 = open_interval a1 bb1 ∖ K_set.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ open_interval a1 bb ∖ K_set) b1 Hb1fam).
Apply Hexb1 to the current goal.
Let bb1 be given.
Assume Hbb1pair.
We prove the intermediate claim Hbb1R: bb1 ∈ R.
An exact proof term for the current goal is (andEL (bb1 ∈ R) (b1 = open_interval a1 bb1 ∖ K_set) Hbb1pair).
We prove the intermediate claim Hb1eq: b1 = open_interval a1 bb1 ∖ K_set.
An exact proof term for the current goal is (andER (bb1 ∈ R) (b1 = open_interval a1 bb1 ∖ K_set) Hbb1pair).
Apply Hexa2 to the current goal.
Let a2 be given.
Assume Ha2pair.
We prove the intermediate claim Ha2R: a2 ∈ R.
An exact proof term for the current goal is (andEL (a2 ∈ R) (b2 ∈ {open_interval a2 b ∖ K_set|b ∈ R}) Ha2pair).
We prove the intermediate claim Hb2fam: b2 ∈ {open_interval a2 b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (andER (a2 ∈ R) (b2 ∈ {open_interval a2 b ∖ K_set|b ∈ R}) Ha2pair).
We prove the intermediate claim Hexb2: ∃bb2 ∈ R, b2 = open_interval a2 bb2 ∖ K_set.
An exact proof term for the current goal is (ReplE R (λbb : set ⇒ open_interval a2 bb ∖ K_set) b2 Hb2fam).
Apply Hexb2 to the current goal.
Let bb2 be given.
Assume Hbb2pair.
We prove the intermediate claim Hbb2R: bb2 ∈ R.
An exact proof term for the current goal is (andEL (bb2 ∈ R) (b2 = open_interval a2 bb2 ∖ K_set) Hbb2pair).
We prove the intermediate claim Hb2eq: b2 = open_interval a2 bb2 ∖ K_set.
An exact proof term for the current goal is (andER (bb2 ∈ R) (b2 = open_interval a2 bb2 ∖ K_set) Hbb2pair).
Set I1 to be the term open_interval a1 bb1.
Set I2 to be the term open_interval a2 bb2.
We prove the intermediate claim HI1Std: I1 ∈ R_standard_basis.
We prove the intermediate claim HI1fam: I1 ∈ {open_interval a1 b|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval a1 b0) bb1 Hbb1R).
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) a1 I1 Ha1R HI1fam).
We prove the intermediate claim HI2Std: I2 ∈ R_standard_basis.
We prove the intermediate claim HI2fam: I2 ∈ {open_interval a2 b|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval a2 b0) bb2 Hbb2R).
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b|b ∈ R}) a2 I2 Ha2R HI2fam).
We prove the intermediate claim HxInB1: x ∈ I1 ∖ K_set.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxInB2: x ∈ I2 ∖ K_set.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim HxInI1: x ∈ I1.
An exact proof term for the current goal is (setminusE1 I1 K_set x HxInB1).
We prove the intermediate claim HxInI2: x ∈ I2.
An exact proof term for the current goal is (setminusE1 I2 K_set x HxInB2).
We prove the intermediate claim HxNotK: x ∉ K_set.
An exact proof term for the current goal is (setminusE2 I1 K_set x HxInB1).
Apply (HstdInt I1 HI1Std I2 HI2Std x HxInI1 HxInI2) to the current goal.
Let I0 be given.
Assume HI0pair.
We prove the intermediate claim HI0Std: I0 ∈ R_standard_basis.
An exact proof term for the current goal is (andEL (I0 ∈ R_standard_basis) (x ∈ I0 ∧ I0 ⊆ I1 ∩ I2) HI0pair).
We prove the intermediate claim HI0rest: x ∈ I0 ∧ I0 ⊆ I1 ∩ I2.
An exact proof term for the current goal is (andER (I0 ∈ R_standard_basis) (x ∈ I0 ∧ I0 ⊆ I1 ∩ I2) HI0pair).
We prove the intermediate claim HxI0: x ∈ I0.
An exact proof term for the current goal is (andEL (x ∈ I0) (I0 ⊆ I1 ∩ I2) HI0rest).
We prove the intermediate claim HI0sub: I0 ⊆ I1 ∩ I2.
An exact proof term for the current goal is (andER (x ∈ I0) (I0 ⊆ I1 ∩ I2) HI0rest).
We prove the intermediate claim Hexc: ∃c ∈ R, I0 ∈ {open_interval c b|b ∈ R}.
An exact proof term for the current goal is (famunionE R (λc0 : set ⇒ {open_interval c0 b|b ∈ R}) I0 HI0Std).
Apply Hexc to the current goal.
Let c be given.
Assume Hcpair.
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (andEL (c ∈ R) (I0 ∈ {open_interval c b|b ∈ R}) Hcpair).
We prove the intermediate claim HI0fam: I0 ∈ {open_interval c b|b ∈ R}.
An exact proof term for the current goal is (andER (c ∈ R) (I0 ∈ {open_interval c b|b ∈ R}) Hcpair).
We prove the intermediate claim Hexd: ∃d ∈ R, I0 = open_interval c d.
An exact proof term for the current goal is (ReplE R (λd0 : set ⇒ open_interval c d0) I0 HI0fam).
Apply Hexd to the current goal.
Let d be given.
Assume Hdpair.
We prove the intermediate claim HdR: d ∈ R.
An exact proof term for the current goal is (andEL (d ∈ R) (I0 = open_interval c d) Hdpair).
We prove the intermediate claim HI0eq: I0 = open_interval c d.
An exact proof term for the current goal is (andER (d ∈ R) (I0 = open_interval c d) Hdpair).
Set Kint to be the term open_interval c d ∖ K_set.
We use Kint to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HKfam: Kint ∈ {open_interval c b ∖ K_set|b ∈ R}.
An exact proof term for the current goal is (ReplI R (λb0 : set ⇒ open_interval c b0 ∖ K_set) d HdR).
We prove the intermediate claim HKinK: Kint ∈ R_K_basis.
An exact proof term for the current goal is (famunionI R (λa0 : set ⇒ {open_interval a0 b ∖ K_set|b ∈ R}) c Kint HcR HKfam).
An exact proof term for the current goal is (binunionI2 R_standard_basis R_K_basis Kint HKinK).
Apply andI to the current goal.
We will prove x ∈ open_interval c d ∖ K_set.
Apply setminusI to the current goal.
We will prove x ∈ open_interval c d.
rewrite the current goal using HI0eq (from right to left).
An exact proof term for the current goal is HxI0.
An exact proof term for the current goal is HxNotK.
Let y be given.
Assume Hy: y ∈ Kint.
We will prove y ∈ b1 ∩ b2.
We prove the intermediate claim HyOpen: y ∈ open_interval c d.
An exact proof term for the current goal is (setminusE1 (open_interval c d) K_set y Hy).
We prove the intermediate claim HyI0: y ∈ I0.
rewrite the current goal using HI0eq (from left to right).
An exact proof term for the current goal is HyOpen.
We prove the intermediate claim HyNotK: y ∉ K_set.
An exact proof term for the current goal is (setminusE2 (open_interval c d) K_set y Hy).
We prove the intermediate claim HyI1I2: y ∈ I1 ∩ I2.
An exact proof term for the current goal is (HI0sub y HyI0).
We prove the intermediate claim HyI1: y ∈ I1.
An exact proof term for the current goal is (binintersectE1 I1 I2 y HyI1I2).
We prove the intermediate claim HyI2: y ∈ I2.
An exact proof term for the current goal is (binintersectE2 I1 I2 y HyI1I2).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (setminusI I1 K_set y HyI1 HyNotK).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (setminusI I2 K_set y HyI2 HyNotK).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
An exact proof term for the current goal is Hb2.
An exact proof term for the current goal is Hb1.
∎