Let X and Tx be given.
Assume Hpara: paracompact_space X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove regular_space X Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U) Hpara).
We will prove one_point_sets_closed X Tx ∧ ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → closed_in X Tx {x}.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (Hausdorff_singletons_closed X Tx x HH HxX).
Let x be given.
Assume HxX: x ∈ X.
Let F be given.
Assume HFcl: closed_in X Tx F.
Assume HxNotF: x ∉ F.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim HFsubX: F ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx F HFcl).
Set U0 to be the term X ∖ F.
We prove the intermediate claim HU0open: open_in X Tx U0.
An exact proof term for the current goal is (open_of_closed_complement X Tx F HFcl).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U0 HU0open).
We prove the intermediate claim HxU0: x ∈ U0.
Apply setminusI to the current goal.
An exact proof term for the current goal is HxX.
An exact proof term for the current goal is HxNotF.
Set sepU to be the term λy : set ⇒ Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty).
Set sepV to be the term λy : set ⇒ Eps_i (λV : set ⇒ (sepU y) ∈ Tx ∧ V ∈ Tx ∧ x ∈ (sepU y) ∧ y ∈ V ∧ (sepU y) ∩ V = Empty).
We prove the intermediate claim HsepVprop: ∀y : set, y ∈ F → (sepU y) ∈ Tx ∧ (sepV y) ∈ Tx ∧ x ∈ (sepU y) ∧ y ∈ (sepV y) ∧ (sepU y) ∩ (sepV y) = Empty.
Let y be given.
Assume HyF: y ∈ F.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HFsubX y HyF).
We prove the intermediate claim Hneq: x ≠ y.
Assume Hxy: x = y.
We prove the intermediate claim HxF: x ∈ F.
rewrite the current goal using Hxy (from left to right).
An exact proof term for the current goal is HyF.
An exact proof term for the current goal is (HxNotF HxF).
We prove the intermediate claim HexSep: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (Hausdorff_space_separation X Tx x y HH HxX HyX Hneq).
We prove the intermediate claim HexU: ∃U : set, ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is HexSep.
We prove the intermediate claim HsepUex: ∃V : set, (sepU y) ∈ Tx ∧ V ∈ Tx ∧ x ∈ (sepU y) ∧ y ∈ V ∧ (sepU y) ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ y ∈ V ∧ U ∩ V = Empty) HexU).
We prove the intermediate claim HexV: ∃V : set, (sepU y) ∈ Tx ∧ V ∈ Tx ∧ x ∈ (sepU y) ∧ y ∈ V ∧ (sepU y) ∩ V = Empty.
An exact proof term for the current goal is HsepUex.
We prove the intermediate claim HsepVex: (sepU y) ∈ Tx ∧ (sepV y) ∈ Tx ∧ x ∈ (sepU y) ∧ y ∈ (sepV y) ∧ (sepU y) ∩ (sepV y) = Empty.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ (sepU y) ∈ Tx ∧ V ∈ Tx ∧ x ∈ (sepU y) ∧ y ∈ V ∧ (sepU y) ∩ V = Empty) HexV).
An exact proof term for the current goal is HsepVex.
Set VFam to be the term {sepV y|y ∈ F}.
Set Cover to be the term {U0} ∪ VFam.
We prove the intermediate claim HCoverOpen: ∀u : set, u ∈ Cover → u ∈ Tx.
Let u be given.
Assume Hu: u ∈ Cover.
We will prove u ∈ Tx.
Apply (binunionE' {U0} VFam u (u ∈ Tx)) to the current goal.
Assume Hu0: u ∈ {U0}.
We prove the intermediate claim Heq: u = U0.
An exact proof term for the current goal is (SingE U0 u Hu0).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is HU0Tx.
Assume HuV: u ∈ VFam.
Apply (ReplE_impred F (λy : set ⇒ sepV y) u HuV (u ∈ Tx)) to the current goal.
Let y be given.
Assume HyF: y ∈ F.
Assume Hueq: u = sepV y.
We prove the intermediate claim Hsep: (sepU y) ∈ Tx ∧ (sepV y) ∈ Tx ∧ x ∈ (sepU y) ∧ y ∈ (sepV y) ∧ (sepU y) ∩ (sepV y) = Empty.
An exact proof term for the current goal is (HsepVprop y HyF).
rewrite the current goal using Hueq (from left to right).
We prove the intermediate claim H1: (((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y) ∧ y ∈ (sepV y)).
An exact proof term for the current goal is (andEL ((((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y) ∧ y ∈ (sepV y))) ((sepU y) ∩ (sepV y) = Empty) Hsep).
We prove the intermediate claim H2: (((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y)).
An exact proof term for the current goal is (andEL ((((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y))) (y ∈ (sepV y)) H1).
We prove the intermediate claim H3: ((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx).
An exact proof term for the current goal is (andEL (((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx)) (x ∈ (sepU y)) H2).
An exact proof term for the current goal is (andER ((sepU y) ∈ Tx) ((sepV y) ∈ Tx) H3).
An exact proof term for the current goal is Hu.
We prove the intermediate claim HCoverCovers: covers X Cover.
Let z be given.
Assume HzX: z ∈ X.
Apply (xm (z ∈ F)) to the current goal.
Assume HzF: z ∈ F.
We use (sepV z) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI2 {U0} VFam (sepV z) (ReplI F (λy : set ⇒ sepV y) z HzF)).
We prove the intermediate claim Hsep: (sepU z) ∈ Tx ∧ (sepV z) ∈ Tx ∧ x ∈ (sepU z) ∧ z ∈ (sepV z) ∧ (sepU z) ∩ (sepV z) = Empty.
An exact proof term for the current goal is (HsepVprop z HzF).
We prove the intermediate claim Hleft: (((sepU z) ∈ Tx ∧ (sepV z) ∈ Tx) ∧ x ∈ (sepU z) ∧ z ∈ (sepV z)).
An exact proof term for the current goal is (andEL ((((sepU z) ∈ Tx ∧ (sepV z) ∈ Tx) ∧ x ∈ (sepU z) ∧ z ∈ (sepV z))) ((sepU z) ∩ (sepV z) = Empty) Hsep).
An exact proof term for the current goal is (andER (((sepU z) ∈ Tx ∧ (sepV z) ∈ Tx) ∧ x ∈ (sepU z)) (z ∈ (sepV z)) Hleft).
Assume HzNotF: ¬ (z ∈ F).
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 {U0} VFam U0 (SingI U0)).
An exact proof term for the current goal is (setminusI X F z HzX HzNotF).
We prove the intermediate claim Hcover: open_cover X Tx Cover.
An exact proof term for the current goal is (andI (∀u : set, u ∈ Cover → u ∈ Tx) (covers X Cover) HCoverOpen HCoverCovers).
We prove the intermediate claim Href: ∃W : set, open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W Cover.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U) Hpara Cover Hcover).
Apply Href to the current goal.
Let W be given.
Assume HW: open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W Cover.
Set WF to be the term {w ∈ W|w ∩ F ≠ Empty}.
Set V to be the term ⋃ WF.
We prove the intermediate claim HWpair: open_cover X Tx W ∧ locally_finite_family X Tx W.
An exact proof term for the current goal is (andEL (open_cover X Tx W ∧ locally_finite_family X Tx W) (refine_of W Cover) HW).
We prove the intermediate claim HWref: refine_of W Cover.
An exact proof term for the current goal is (andER (open_cover X Tx W ∧ locally_finite_family X Tx W) (refine_of W Cover) HW).
We prove the intermediate claim HWcover: open_cover X Tx W.
An exact proof term for the current goal is (andEL (open_cover X Tx W) (locally_finite_family X Tx W) HWpair).
We prove the intermediate claim HLFW: locally_finite_family X Tx W.
An exact proof term for the current goal is (andER (open_cover X Tx W) (locally_finite_family X Tx W) HWpair).
We prove the intermediate claim HWopen: ∀w : set, w ∈ W → w ∈ Tx.
An exact proof term for the current goal is (andEL (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcover).
We prove the intermediate claim HWcovers: covers X W.
An exact proof term for the current goal is (andER (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcover).
We prove the intermediate claim HWFsubW: WF ⊆ W.
An exact proof term for the current goal is (Sep_Subq W (λw : set ⇒ w ∩ F ≠ Empty)).
We prove the intermediate claim HLF_WF: locally_finite_family X Tx WF.
An exact proof term for the current goal is (locally_finite_subfamily X Tx W WF HLFW HWFsubW).
We prove the intermediate claim HWFsubTx: WF ⊆ Tx.
Let w be given.
Assume HwWF: w ∈ WF.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (SepE1 W (λw0 : set ⇒ w0 ∩ F ≠ Empty) w HwWF).
An exact proof term for the current goal is (HWopen w HwW).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx WF HTx HWFsubTx).
We prove the intermediate claim HVsubX: V ⊆ X.
Let z be given.
Assume HzV: z ∈ V.
Apply (UnionE_impred WF z HzV) to the current goal.
Let w be given.
Assume Hzw: z ∈ w.
Assume HwWF: w ∈ WF.
We prove the intermediate claim HwTx: w ∈ Tx.
An exact proof term for the current goal is (HWFsubTx w HwWF).
We prove the intermediate claim HwsubX: w ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx w HTx HwTx).
An exact proof term for the current goal is (HwsubX z Hzw).
We prove the intermediate claim HFsubV: F ⊆ V.
Let y be given.
Assume HyF: y ∈ F.
We will prove y ∈ V.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HFsubX y HyF).
Apply (HWcovers y HyX) to the current goal.
Let w be given.
Assume HwW: w ∈ W ∧ y ∈ w.
We prove the intermediate claim HwInW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (y ∈ w) HwW).
We prove the intermediate claim Hyw: y ∈ w.
An exact proof term for the current goal is (andER (w ∈ W) (y ∈ w) HwW).
We prove the intermediate claim HwFnon: w ∩ F ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (w ∩ F) y (binintersectI w F y Hyw HyF)).
We prove the intermediate claim HwWF: w ∈ WF.
An exact proof term for the current goal is (SepI W (λw0 : set ⇒ w0 ∩ F ≠ Empty) w HwInW HwFnon).
An exact proof term for the current goal is (UnionI WF y w Hyw HwWF).
Set ClWF to be the term {closure_of X Tx w|w ∈ WF}.
Set C to be the term ⋃ ClWF.
We prove the intermediate claim HWFsubX: ∀w : set, w ∈ WF → w ⊆ X.
Let w be given.
Assume HwWF: w ∈ WF.
We prove the intermediate claim HwTx: w ∈ Tx.
An exact proof term for the current goal is (HWFsubTx w HwWF).
An exact proof term for the current goal is (topology_elem_subset X Tx w HTx HwTx).
We prove the intermediate claim HVdef: V = ⋃ WF.
Use reflexivity.
We prove the intermediate claim HclVsubC': closure_of X Tx (⋃ WF) ⊆ C.
An exact proof term for the current goal is (closure_Union_locally_finite_subset_Union_closures X Tx WF HWFsubX HLF_WF).
We prove the intermediate claim HclVsubC: closure_of X Tx V ⊆ C.
rewrite the current goal using HVdef (from left to right).
An exact proof term for the current goal is HclVsubC'.
We prove the intermediate claim HCsubclV: C ⊆ closure_of X Tx V.
Let z be given.
Assume HzC: z ∈ C.
We will prove z ∈ closure_of X Tx V.
Apply (UnionE_impred ClWF z HzC) to the current goal.
Let clw be given.
Assume Hzclw: z ∈ clw.
Assume Hclw: clw ∈ ClWF.
Apply (ReplE_impred WF (λw : set ⇒ closure_of X Tx w) clw Hclw) to the current goal.
Let w be given.
Assume HwWF: w ∈ WF.
Assume Hclweq: clw = closure_of X Tx w.
We prove the intermediate claim Hzclw2: z ∈ closure_of X Tx w.
rewrite the current goal using Hclweq (from right to left).
An exact proof term for the current goal is Hzclw.
We prove the intermediate claim HwsubV: w ⊆ V.
Let t be given.
Assume Htw: t ∈ w.
An exact proof term for the current goal is (UnionI WF t w Htw HwWF).
We prove the intermediate claim Hclwsub: closure_of X Tx w ⊆ closure_of X Tx V.
An exact proof term for the current goal is (closure_monotone X Tx w V HTx HwsubV HVsubX).
An exact proof term for the current goal is (Hclwsub z Hzclw2).
We prove the intermediate claim HCeq: closure_of X Tx V = C.
Apply set_ext to the current goal.
An exact proof term for the current goal is HclVsubC.
An exact proof term for the current goal is HCsubclV.
We prove the intermediate claim HCclosed: closed_in X Tx C.
rewrite the current goal using HCeq (from right to left).
An exact proof term for the current goal is (closure_is_closed X Tx V HTx HVsubX).
Set U to be the term X ∖ C.
We prove the intermediate claim HUopen: open_in X Tx U.
An exact proof term for the current goal is (open_of_closed_complement X Tx C HCclosed).
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx U HUopen).
We prove the intermediate claim HxNotC: x ∉ C.
Assume HxC: x ∈ C.
Apply (UnionE_impred ClWF x HxC) to the current goal.
Let clw be given.
Assume Hxclw: x ∈ clw.
Assume Hclw: clw ∈ ClWF.
Apply (ReplE_impred WF (λw : set ⇒ closure_of X Tx w) clw Hclw) to the current goal.
Let w be given.
Assume HwWF: w ∈ WF.
Assume Hclweq: clw = closure_of X Tx w.
We prove the intermediate claim Hxclw2: x ∈ closure_of X Tx w.
rewrite the current goal using Hclweq (from right to left).
An exact proof term for the current goal is Hxclw.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (HWFsubW w HwWF).
We prove the intermediate claim Hexu: ∃u : set, u ∈ Cover ∧ w ⊆ u.
An exact proof term for the current goal is (HWref w HwW).
Apply Hexu to the current goal.
Let u be given.
Assume Hu: u ∈ Cover ∧ w ⊆ u.
We prove the intermediate claim HuCover: u ∈ Cover.
An exact proof term for the current goal is (andEL (u ∈ Cover) (w ⊆ u) Hu).
We prove the intermediate claim Hwsubu: w ⊆ u.
An exact proof term for the current goal is (andER (u ∈ Cover) (w ⊆ u) Hu).
We prove the intermediate claim HxNotclw: x ∉ closure_of X Tx w.
Apply (binunionE {U0} VFam u HuCover) to the current goal.
Assume Hu0: u ∈ {U0}.
We prove the intermediate claim Hueq: u = U0.
An exact proof term for the current goal is (SingE U0 u Hu0).
We prove the intermediate claim HwsubU0: w ⊆ U0.
Let t be given.
Assume Htw: t ∈ w.
We will prove t ∈ U0.
rewrite the current goal using Hueq (from right to left).
An exact proof term for the current goal is (Hwsubu t Htw).
We prove the intermediate claim HwFnon: w ∩ F ≠ Empty.
An exact proof term for the current goal is (SepE2 W (λw0 : set ⇒ w0 ∩ F ≠ Empty) w HwWF).
We prove the intermediate claim HwFsubEmpty: w ∩ F ⊆ Empty.
Let t be given.
Assume Ht: t ∈ w ∩ F.
We will prove t ∈ Empty.
We prove the intermediate claim Htpair: t ∈ w ∧ t ∈ F.
An exact proof term for the current goal is (binintersectE w F t Ht).
We prove the intermediate claim Htw: t ∈ w.
An exact proof term for the current goal is (andEL (t ∈ w) (t ∈ F) Htpair).
We prove the intermediate claim HtF: t ∈ F.
An exact proof term for the current goal is (andER (t ∈ w) (t ∈ F) Htpair).
We prove the intermediate claim HtU0: t ∈ U0.
An exact proof term for the current goal is (HwsubU0 t Htw).
We prove the intermediate claim HtNotF: t ∉ F.
An exact proof term for the current goal is (setminusE2 X F t HtU0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HtNotF HtF).
We prove the intermediate claim HwFEmpty: w ∩ F = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (w ∩ F) HwFsubEmpty).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HwFnon HwFEmpty).
Assume HuV: u ∈ VFam.
Apply (ReplE_impred F (λy0 : set ⇒ sepV y0) u HuV (x ∉ closure_of X Tx w)) to the current goal.
Let y be given.
Assume HyF: y ∈ F.
Assume Hueq: u = sepV y.
We prove the intermediate claim HwsubVy: w ⊆ sepV y.
Let t be given.
Assume Htw: t ∈ w.
We will prove t ∈ sepV y.
rewrite the current goal using Hueq (from right to left).
An exact proof term for the current goal is (Hwsubu t Htw).
We prove the intermediate claim Hsep: (sepU y) ∈ Tx ∧ (sepV y) ∈ Tx ∧ x ∈ (sepU y) ∧ y ∈ (sepV y) ∧ (sepU y) ∩ (sepV y) = Empty.
An exact proof term for the current goal is (HsepVprop y HyF).
We prove the intermediate claim Hleft: (((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y) ∧ y ∈ (sepV y)).
An exact proof term for the current goal is (andEL ((((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y) ∧ y ∈ (sepV y))) ((sepU y) ∩ (sepV y) = Empty) Hsep).
We prove the intermediate claim Hdisj: (sepU y) ∩ (sepV y) = Empty.
An exact proof term for the current goal is (andER ((((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y) ∧ y ∈ (sepV y))) ((sepU y) ∩ (sepV y) = Empty) Hsep).
We prove the intermediate claim Htmp: (((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y)).
An exact proof term for the current goal is (andEL ((((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx) ∧ x ∈ (sepU y))) (y ∈ (sepV y)) Hleft).
We prove the intermediate claim HUV: ((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx).
An exact proof term for the current goal is (andEL (((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx)) (x ∈ (sepU y)) Htmp).
We prove the intermediate claim HUyTx: (sepU y) ∈ Tx.
An exact proof term for the current goal is (andEL ((sepU y) ∈ Tx) ((sepV y) ∈ Tx) HUV).
We prove the intermediate claim HxUy: x ∈ sepU y.
An exact proof term for the current goal is (andER (((sepU y) ∈ Tx ∧ (sepV y) ∈ Tx)) (x ∈ (sepU y)) Htmp).
We prove the intermediate claim HUywEmpty: (sepU y) ∩ w = Empty.
Apply Empty_Subq_eq to the current goal.
Let t be given.
Assume Ht: t ∈ (sepU y) ∩ w.
We will prove t ∈ Empty.
We prove the intermediate claim Htpair: t ∈ sepU y ∧ t ∈ w.
An exact proof term for the current goal is (binintersectE (sepU y) w t Ht).
We prove the intermediate claim HtUy: t ∈ sepU y.
An exact proof term for the current goal is (andEL (t ∈ sepU y) (t ∈ w) Htpair).
We prove the intermediate claim Htw: t ∈ w.
An exact proof term for the current goal is (andER (t ∈ sepU y) (t ∈ w) Htpair).
We prove the intermediate claim HtVy: t ∈ sepV y.
An exact proof term for the current goal is (HwsubVy t Htw).
We prove the intermediate claim HtUyVy: t ∈ (sepU y) ∩ (sepV y).
An exact proof term for the current goal is (binintersectI (sepU y) (sepV y) t HtUy HtVy).
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HtUyVy.
We prove the intermediate claim Hclprop: ∀U : set, U ∈ Tx → x ∈ U → U ∩ w ≠ Empty.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U : set, U ∈ Tx → x0 ∈ U → U ∩ w ≠ Empty) x Hxclw2).
We prove the intermediate claim Hnon: (sepU y) ∩ w ≠ Empty.
An exact proof term for the current goal is (Hclprop (sepU y) HUyTx HxUy).
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnon HUywEmpty).
An exact proof term for the current goal is (HxNotclw Hxclw2).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (setminusI X C x HxX HxNotC).
We prove the intermediate claim HVsubC: V ⊆ C.
Let z be given.
Assume HzV: z ∈ V.
We will prove z ∈ C.
Apply (UnionE_impred WF z HzV) to the current goal.
Let w be given.
Assume Hzw: z ∈ w.
Assume HwWF: w ∈ WF.
We prove the intermediate claim HwsubX: w ⊆ X.
An exact proof term for the current goal is (HWFsubX w HwWF).
We prove the intermediate claim Hzclw: z ∈ closure_of X Tx w.
An exact proof term for the current goal is (subset_of_closure X Tx w HTx HwsubX z Hzw).
An exact proof term for the current goal is (UnionI ClWF z (closure_of X Tx w) Hzclw (ReplI WF (λw0 : set ⇒ closure_of X Tx w0) w HwWF)).
We prove the intermediate claim HUdisjV: U ∩ V = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ V.
We will prove z ∈ Empty.
We prove the intermediate claim Hzpair: z ∈ U ∧ z ∈ V.
An exact proof term for the current goal is (binintersectE U V z Hz).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (andEL (z ∈ U) (z ∈ V) Hzpair).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (andER (z ∈ U) (z ∈ V) Hzpair).
We prove the intermediate claim HzNotC: z ∉ C.
An exact proof term for the current goal is (setminusE2 X C z HzU).
We prove the intermediate claim HzC: z ∈ C.
An exact proof term for the current goal is (HVsubC z HzV).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HzNotC HzC).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is HUTx.
An exact proof term for the current goal is HVTx.
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is HFsubV.
An exact proof term for the current goal is HUdisjV.
∎