Let X, Tx, Y and Ty be given.
Assume Hlc: locally_compact X Tx.
Assume HHx: Hausdorff_space X Tx.
Assume HTy: topology_on Y Ty.
Set CXY to be the term continuous_function_space X Tx Y Ty.
Set Tco to be the term compact_open_topology_C X Tx Y Ty.
Set Dom to be the term setprod X CXY.
Set Tdom to be the term product_topology X Tx CXY Tco.
We will prove continuous_map Dom Tdom Y Ty (compact_open_evaluation_map X Tx Y Ty).
We will prove topology_on Dom Tdom ∧ topology_on Y Ty ∧ function_on (compact_open_evaluation_map X Tx Y Ty) Dom Y ∧ ∀V : set, V ∈ Ty → preimage_of Dom (compact_open_evaluation_map X Tx Y Ty) V ∈ Tdom.
We prove the intermediate claim Hpart1: topology_on Dom Tdom ∧ topology_on Y Ty.
Apply andI to the current goal.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_compact_topology X Tx Hlc).
We prove the intermediate claim HTco: topology_on CXY Tco.
An exact proof term for the current goal is (compact_open_topology_C_is_topology X Tx Y Ty HTx HTy).
An exact proof term for the current goal is (product_topology_is_topology X Tx CXY Tco HTx HTco).
An exact proof term for the current goal is HTy.
We prove the intermediate claim Hpart2: (topology_on Dom Tdom ∧ topology_on Y Ty) ∧ function_on (compact_open_evaluation_map X Tx Y Ty) Dom Y.
Apply andI to the current goal.
An exact proof term for the current goal is Hpart1.
We will prove function_on (compact_open_evaluation_map X Tx Y Ty) Dom Y.
Let p be given.
Assume Hp: p ∈ Dom.
We will prove apply_fun (compact_open_evaluation_map X Tx Y Ty) p ∈ Y.
We prove the intermediate claim Hp0X: p 0 ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ CXY) p Hp).
We prove the intermediate claim Hp1C: p 1 ∈ CXY.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ CXY) p Hp).
We prove the intermediate claim HCsub: CXY ⊆ function_space X Y.
An exact proof term for the current goal is (continuous_function_space_sub X Tx Y Ty).
We prove the intermediate claim Hp1FS: p 1 ∈ function_space X Y.
An exact proof term for the current goal is (HCsub (p 1) Hp1C).
We prove the intermediate claim Hp1fun: function_on (p 1) X Y.
An exact proof term for the current goal is (function_on_of_function_space (p 1) X Y Hp1FS).
We prove the intermediate claim Hevaldef: compact_open_evaluation_map X Tx Y Ty = graph Dom (λq : set ⇒ apply_fun (q 1) (q 0)).
Use reflexivity.
rewrite the current goal using Hevaldef (from left to right).
rewrite the current goal using (apply_fun_graph Dom (λq : set ⇒ apply_fun (q 1) (q 0)) p Hp) (from left to right).
An exact proof term for the current goal is (Hp1fun (p 0) Hp0X).
Apply andI to the current goal.
An exact proof term for the current goal is Hpart2.
Let V be given.
Assume HV: V ∈ Ty.
We will prove preimage_of Dom (compact_open_evaluation_map X Tx Y Ty) V ∈ Tdom.
Set Pre to be the term preimage_of Dom (compact_open_evaluation_map X Tx Y Ty) V.
We will prove Pre ∈ generated_topology Dom (product_subbasis X Tx CXY Tco).
We will prove Pre ∈ {U0 ∈ 𝒫 Dom|∀p0 ∈ U0, ∃b ∈ product_subbasis X Tx CXY Tco, p0 ∈ b ∧ b ⊆ U0}.
Apply SepI to the current goal.
Apply PowerI to the current goal.
Let p0 be given.
Assume Hp0: p0 ∈ Pre.
An exact proof term for the current goal is (SepE1 Dom (λq : set ⇒ apply_fun (compact_open_evaluation_map X Tx Y Ty) q ∈ V) p0 Hp0).
Let p0 be given.
Assume Hp0: p0 ∈ Pre.
We will prove ∃b ∈ product_subbasis X Tx CXY Tco, p0 ∈ b ∧ b ⊆ Pre.
We prove the intermediate claim Hp0Dom: p0 ∈ Dom.
An exact proof term for the current goal is (SepE1 Dom (λq : set ⇒ apply_fun (compact_open_evaluation_map X Tx Y Ty) q ∈ V) p0 Hp0).
We prove the intermediate claim Hp0img: apply_fun (compact_open_evaluation_map X Tx Y Ty) p0 ∈ V.
An exact proof term for the current goal is (SepE2 Dom (λq : set ⇒ apply_fun (compact_open_evaluation_map X Tx Y Ty) q ∈ V) p0 Hp0).
Set x0 to be the term p0 0.
Set f0 to be the term p0 1.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (ap0_Sigma X (λ_ : set ⇒ CXY) p0 Hp0Dom).
We prove the intermediate claim Hf0C: f0 ∈ CXY.
An exact proof term for the current goal is (ap1_Sigma X (λ_ : set ⇒ CXY) p0 Hp0Dom).
We prove the intermediate claim Hf0Dom: f0 ∈ function_space X Y.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λg : set ⇒ continuous_map X Tx Y Ty g) f0 Hf0C).
We prove the intermediate claim Hf0cont: continuous_map X Tx Y Ty f0.
An exact proof term for the current goal is (SepE2 (function_space X Y) (λg : set ⇒ continuous_map X Tx Y Ty g) f0 Hf0C).
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (locally_compact_topology X Tx Hlc).
We prove the intermediate claim Hevaldef0: compact_open_evaluation_map X Tx Y Ty = graph Dom (λq : set ⇒ apply_fun (q 1) (q 0)).
Use reflexivity.
We prove the intermediate claim HimgEq: apply_fun (compact_open_evaluation_map X Tx Y Ty) p0 = apply_fun f0 x0.
rewrite the current goal using Hevaldef0 (from left to right).
rewrite the current goal using (apply_fun_graph Dom (λq : set ⇒ apply_fun (q 1) (q 0)) p0 Hp0Dom) (from left to right).
Use reflexivity.
We prove the intermediate claim Hf0x0V: apply_fun f0 x0 ∈ V.
rewrite the current goal using HimgEq (from right to left).
An exact proof term for the current goal is Hp0img.
Set W0 to be the term preimage_of X f0 V.
We prove the intermediate claim HW0Tx: W0 ∈ Tx.
An exact proof term for the current goal is (continuous_map_preimage X Tx Y Ty f0 Hf0cont V HV).
We prove the intermediate claim Hx0W0: x0 ∈ W0.
An exact proof term for the current goal is (SepI X (λx : set ⇒ apply_fun f0 x ∈ V) x0 Hx0X Hf0x0V).
Apply (locally_compact_local X Tx x0 Hlc Hx0X) to the current goal.
Let U1 be given.
Assume HU1pack: U1 ∈ Tx ∧ x0 ∈ U1 ∧ compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1)).
We prove the intermediate claim HU1pair: U1 ∈ Tx ∧ x0 ∈ U1.
An exact proof term for the current goal is (andEL (U1 ∈ Tx ∧ x0 ∈ U1) (compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1))) HU1pack).
We prove the intermediate claim HU1Tx: U1 ∈ Tx.
An exact proof term for the current goal is (andEL (U1 ∈ Tx) (x0 ∈ U1) HU1pair).
We prove the intermediate claim Hx0U1: x0 ∈ U1.
An exact proof term for the current goal is (andER (U1 ∈ Tx) (x0 ∈ U1) HU1pair).
Set K1 to be the term closure_of X Tx U1.
Set TK1 to be the term subspace_topology X Tx K1.
We prove the intermediate claim HK1comp: compact_space K1 TK1.
An exact proof term for the current goal is (andER (U1 ∈ Tx ∧ x0 ∈ U1) (compact_space (closure_of X Tx U1) (subspace_topology X Tx (closure_of X Tx U1))) HU1pack).
We prove the intermediate claim HK1subX: K1 ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx U1 HTx).
We prove the intermediate claim HHK1: Hausdorff_space K1 TK1.
An exact proof term for the current goal is (ex17_12_subspace_Hausdorff X Tx K1 HHx HK1subX).
We prove the intermediate claim HnormK1: normal_space K1 TK1.
An exact proof term for the current goal is (compact_Hausdorff_normal K1 TK1 HK1comp HHK1).
We prove the intermediate claim HregK1: regular_space K1 TK1.
An exact proof term for the current goal is (normal_space_implies_regular K1 TK1 HnormK1).
Set W to be the term W0 ∩ U1.
We prove the intermediate claim HWTx: W ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx W0 U1 HTx HW0Tx HU1Tx).
Set O1 to be the term W ∩ K1.
We prove the intermediate claim HO1: O1 ∈ TK1.
An exact proof term for the current goal is (subspace_topologyI X Tx K1 W HWTx).
We prove the intermediate claim Hx0K1: x0 ∈ K1.
An exact proof term for the current goal is ((closure_contains_set X Tx U1 HTx (topology_elem_subset X Tx U1 HTx HU1Tx)) x0 Hx0U1).
We prove the intermediate claim Hx0O1: x0 ∈ O1.
An exact proof term for the current goal is (binintersectI W K1 x0 (binintersectI W0 U1 x0 Hx0W0 Hx0U1) Hx0K1).
Apply (regular_space_open_nbhd_closure_sub K1 TK1 O1 x0 HregK1 HO1 Hx0O1) to the current goal.
Let V1 be given.
Assume HV1pack: V1 ∈ TK1 ∧ x0 ∈ V1 ∧ closure_of K1 TK1 V1 ⊆ O1.
We prove the intermediate claim HV1pair: V1 ∈ TK1 ∧ x0 ∈ V1.
An exact proof term for the current goal is (andEL (V1 ∈ TK1 ∧ x0 ∈ V1) (closure_of K1 TK1 V1 ⊆ O1) HV1pack).
We prove the intermediate claim HV1TK1: V1 ∈ TK1.
An exact proof term for the current goal is (andEL (V1 ∈ TK1) (x0 ∈ V1) HV1pair).
We prove the intermediate claim Hx0V1: x0 ∈ V1.
An exact proof term for the current goal is (andER (V1 ∈ TK1) (x0 ∈ V1) HV1pair).
We prove the intermediate claim HclV1subO1: closure_of K1 TK1 V1 ⊆ O1.
An exact proof term for the current goal is (andER (V1 ∈ TK1 ∧ x0 ∈ V1) (closure_of K1 TK1 V1 ⊆ O1) HV1pack).
Apply (subspace_topologyE X Tx K1 V1 HV1TK1) to the current goal.
Let U2 be given.
Assume HU2pack: U2 ∈ Tx ∧ V1 = U2 ∩ K1.
We prove the intermediate claim HU2Tx: U2 ∈ Tx.
An exact proof term for the current goal is (andEL (U2 ∈ Tx) (V1 = U2 ∩ K1) HU2pack).
We prove the intermediate claim HV1eq: V1 = U2 ∩ K1.
An exact proof term for the current goal is (andER (U2 ∈ Tx) (V1 = U2 ∩ K1) HU2pack).
Set U to be the term U2 ∩ U1.
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx U2 U1 HTx HU2Tx HU1Tx).
We prove the intermediate claim Hx0U2: x0 ∈ U2.
We prove the intermediate claim Hx0U2K1: x0 ∈ U2 ∩ K1.
rewrite the current goal using HV1eq (from right to left).
An exact proof term for the current goal is Hx0V1.
An exact proof term for the current goal is (binintersectE1 U2 K1 x0 Hx0U2K1).
We prove the intermediate claim Hx0U: x0 ∈ U.
An exact proof term for the current goal is (binintersectI U2 U1 x0 Hx0U2 Hx0U1).
Set K to be the term closure_of X Tx U.
We prove the intermediate claim HV1subK1: V1 ⊆ K1.
An exact proof term for the current goal is (subspace_topology_subset X Tx K1 V1 HV1TK1).
We prove the intermediate claim HV1subX: V1 ⊆ X.
Let t be given.
Assume Ht: t ∈ V1.
An exact proof term for the current goal is (HK1subX t (HV1subK1 t Ht)).
We prove the intermediate claim HUsubV1: U ⊆ V1.
Let t be given.
Assume HtU: t ∈ U.
We prove the intermediate claim HtU2: t ∈ U2.
An exact proof term for the current goal is (binintersectE1 U2 U1 t HtU).
We prove the intermediate claim HtU1: t ∈ U1.
An exact proof term for the current goal is (binintersectE2 U2 U1 t HtU).
We prove the intermediate claim HU1subK1': U1 ⊆ K1.
An exact proof term for the current goal is (closure_contains_set X Tx U1 HTx (topology_elem_subset X Tx U1 HTx HU1Tx)).
We prove the intermediate claim HtK1: t ∈ K1.
An exact proof term for the current goal is (HU1subK1' t HtU1).
rewrite the current goal using HV1eq (from left to right).
An exact proof term for the current goal is (binintersectI U2 K1 t HtU2 HtK1).
We prove the intermediate claim HclUsub_clV1: K ⊆ closure_of X Tx V1.
An exact proof term for the current goal is (closure_monotone X Tx U V1 HTx HUsubV1 HV1subX).
We prove the intermediate claim HK1closed: closed_in X Tx K1.
An exact proof term for the current goal is (compact_subspace_in_Hausdorff_closed X Tx K1 HHx HK1subX HK1comp).
We prove the intermediate claim HclV1subK1: closure_of X Tx V1 ⊆ K1.
An exact proof term for the current goal is (closure_subset_of_closed_superset X Tx V1 K1 HTx HV1subK1 HK1closed).
We prove the intermediate claim HclV1inK1: closure_of X Tx V1 ⊆ K1.
An exact proof term for the current goal is HclV1subK1.
We prove the intermediate claim HclV1eq: closure_of K1 TK1 V1 = closure_of X Tx V1.
We prove the intermediate claim Heq0: closure_of K1 TK1 V1 = (closure_of X Tx V1) ∩ K1.
An exact proof term for the current goal is (closure_in_subspace X Tx K1 V1 HTx HK1subX HV1subK1).
rewrite the current goal using Heq0 (from left to right).
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ (closure_of X Tx V1) ∩ K1.
An exact proof term for the current goal is (binintersectE1 (closure_of X Tx V1) K1 t Ht).
Let t be given.
Assume Ht: t ∈ closure_of X Tx V1.
An exact proof term for the current goal is (binintersectI (closure_of X Tx V1) K1 t Ht (HclV1inK1 t Ht)).
We prove the intermediate claim HO1subW: O1 ⊆ W.
An exact proof term for the current goal is (binintersect_Subq_1 W K1).
We prove the intermediate claim HWsubW0: W ⊆ W0.
An exact proof term for the current goal is (binintersect_Subq_1 W0 U1).
We prove the intermediate claim HclV1subW0: closure_of X Tx V1 ⊆ W0.
Let t be given.
Assume Ht: t ∈ closure_of X Tx V1.
We prove the intermediate claim HtclK1: t ∈ closure_of K1 TK1 V1.
rewrite the current goal using HclV1eq (from left to right).
An exact proof term for the current goal is Ht.
An exact proof term for the current goal is (HWsubW0 t (HO1subW t (HclV1subO1 t HtclK1))).
We prove the intermediate claim HKsubW0: K ⊆ W0.
Let t be given.
Assume HtK: t ∈ K.
An exact proof term for the current goal is (HclV1subW0 t (HclUsub_clV1 t HtK)).
We prove the intermediate claim HUsubX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUTx).
We prove the intermediate claim HKclosedX: closed_in X Tx K.
An exact proof term for the current goal is (closure_is_closed X Tx U HTx HUsubX).
We prove the intermediate claim HKsubK1: K ⊆ K1.
We prove the intermediate claim HUsubU1: U ⊆ U1.
An exact proof term for the current goal is (binintersect_Subq_2 U2 U1).
We prove the intermediate claim HU1subX: U1 ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U1 HTx HU1Tx).
An exact proof term for the current goal is (closure_monotone X Tx U U1 HTx HUsubU1 HU1subX).
We prove the intermediate claim HKclosedK1: closed_in K1 TK1 K.
Apply (iffER (closed_in K1 TK1 K) (∃C : set, closed_in X Tx C ∧ K = C ∩ K1) (closed_in_subspace_iff_intersection X Tx K1 K HTx HK1subX)) to the current goal.
We use K to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HKclosedX.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ K.
An exact proof term for the current goal is (binintersectI K K1 t Ht (HKsubK1 t Ht)).
Let t be given.
Assume Ht: t ∈ K ∩ K1.
An exact proof term for the current goal is (binintersectE1 K K1 t Ht).
We prove the intermediate claim HKcomp_in_K1: compact_space K (subspace_topology K1 TK1 K).
An exact proof term for the current goal is (closed_subspace_compact K1 TK1 K HK1comp HKclosedK1).
We prove the intermediate claim HKcomp: compact_space K (subspace_topology X Tx K).
We prove the intermediate claim HeqTop: subspace_topology K1 TK1 K = subspace_topology X Tx K.
An exact proof term for the current goal is (ex16_1_subspace_transitive X Tx K1 K HTx HK1subX HKsubK1).
rewrite the current goal using HeqTop (from right to left).
An exact proof term for the current goal is HKcomp_in_K1.
Set S0 to be the term {g ∈ function_space X Y|K ⊆ preimage_of X g V}.
We prove the intermediate claim HS0inSub: S0 ∈ compact_open_subbasis X Tx Y Ty.
We prove the intermediate claim HdefCOSub: compact_open_subbasis X Tx Y Ty = {S ∈ 𝒫 (function_space X Y)|∃K0 U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S = {f ∈ function_space X Y|K0 ⊆ preimage_of X f U0}}.
Use reflexivity.
rewrite the current goal using HdefCOSub (from left to right).
Apply SepI to the current goal.
Apply PowerI to the current goal.
Let g be given.
Assume Hg: g ∈ S0.
An exact proof term for the current goal is (SepE1 (function_space X Y) (λg0 : set ⇒ K ⊆ preimage_of X g0 V) g Hg).
We prove the intermediate claim HexS0: ∃K0 U0 : set, compact_space K0 (subspace_topology X Tx K0) ∧ K0 ⊆ X ∧ U0 ∈ Ty ∧ S0 = {f ∈ function_space X Y|K0 ⊆ preimage_of X f U0}.
We use K to witness the existential quantifier.
We use V to witness the existential quantifier.
We prove the intermediate claim HKsubX': K ⊆ X.
An exact proof term for the current goal is (closure_in_space X Tx U HTx).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HKcomp.
An exact proof term for the current goal is HKsubX'.
An exact proof term for the current goal is HV.
Use reflexivity.
An exact proof term for the current goal is HexS0.
We prove the intermediate claim HSsub: subbasis_on (function_space X Y) (compact_open_subbasis X Tx Y Ty).
An exact proof term for the current goal is (compact_open_subbasis_is_subbasis X Tx Y Ty HTx HTy).
We prove the intermediate claim HS0openFS: S0 ∈ compact_convergence_topology X Tx Y Ty.
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis (function_space X Y) (compact_open_subbasis X Tx Y Ty) S0 HSsub HS0inSub).
Set Wf to be the term S0 ∩ CXY.
We prove the intermediate claim HWfTco: Wf ∈ Tco.
An exact proof term for the current goal is (subspace_topologyI (function_space X Y) (compact_convergence_topology X Tx Y Ty) CXY S0 HS0openFS).
Set b to be the term rectangle_set U Wf.
We use b to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hbeq: b = rectangle_set U Wf.
Use reflexivity.
rewrite the current goal using Hbeq (from left to right).
We will prove rectangle_set U Wf ∈ ⋃U0 ∈ Tx{rectangle_set U0 V0|V0 ∈ Tco}.
Apply (famunionI Tx (λU0 : set ⇒ {rectangle_set U0 V0|V0 ∈ Tco}) U (rectangle_set U Wf) HUTx) to the current goal.
An exact proof term for the current goal is (ReplI Tco (λV0 : set ⇒ rectangle_set U V0) Wf HWfTco).
Apply andI to the current goal.
We prove the intermediate claim Hx0U': x0 ∈ U.
An exact proof term for the current goal is Hx0U.
We prove the intermediate claim Hf0S0: f0 ∈ S0.
Apply SepI to the current goal.
An exact proof term for the current goal is Hf0Dom.
Let t be given.
Assume HtK: t ∈ K.
An exact proof term for the current goal is (HKsubW0 t HtK).
We prove the intermediate claim Hf0Wf: f0 ∈ Wf.
An exact proof term for the current goal is (binintersectI S0 CXY f0 Hf0S0 Hf0C).
We prove the intermediate claim HpEta: p0 = (x0,f0).
rewrite the current goal using (setprod_eta X CXY p0 Hp0Dom) (from right to left).
Use reflexivity.
rewrite the current goal using HpEta (from left to right).
An exact proof term for the current goal is (tuple_2_rectangle_set U Wf x0 f0 Hx0U' Hf0Wf).
Let q be given.
Assume Hq: q ∈ b.
We will prove q ∈ Pre.
We prove the intermediate claim HqU: q 0 ∈ U.
An exact proof term for the current goal is (ap0_Sigma U (λ_ : set ⇒ Wf) q Hq).
We prove the intermediate claim HqWf: q 1 ∈ Wf.
An exact proof term for the current goal is (ap1_Sigma U (λ_ : set ⇒ Wf) q Hq).
We prove the intermediate claim HqS0: q 1 ∈ S0.
An exact proof term for the current goal is (binintersectE1 S0 CXY (q 1) HqWf).
We prove the intermediate claim HqCXY: q 1 ∈ CXY.
An exact proof term for the current goal is (binintersectE2 S0 CXY (q 1) HqWf).
We prove the intermediate claim HS0K: K ⊆ preimage_of X (q 1) V.
An exact proof term for the current goal is (SepE2 (function_space X Y) (λg0 : set ⇒ K ⊆ preimage_of X g0 V) (q 1) HqS0).
We prove the intermediate claim HUsubK: U ⊆ K.
An exact proof term for the current goal is (closure_contains_set X Tx U HTx HUsubX).
We prove the intermediate claim Hq0K: q 0 ∈ K.
An exact proof term for the current goal is (HUsubK (q 0) HqU).
We prove the intermediate claim Hq0pre: q 0 ∈ preimage_of X (q 1) V.
An exact proof term for the current goal is (HS0K (q 0) Hq0K).
We prove the intermediate claim Hq1q0V: apply_fun (q 1) (q 0) ∈ V.
An exact proof term for the current goal is (SepE2 X (λx : set ⇒ apply_fun (q 1) x ∈ V) (q 0) Hq0pre).
We prove the intermediate claim HUsX: U ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx U HTx HUTx).
We prove the intermediate claim HWfsubCXY: Wf ⊆ CXY.
An exact proof term for the current goal is (binintersect_Subq_2 S0 CXY).
We prove the intermediate claim HqDom: q ∈ Dom.
An exact proof term for the current goal is (setprod_Subq U Wf X CXY HUsX HWfsubCXY q Hq).
We prove the intermediate claim Himgq: apply_fun (compact_open_evaluation_map X Tx Y Ty) q ∈ V.
rewrite the current goal using Hevaldef0 (from left to right).
rewrite the current goal using (apply_fun_graph Dom (λq0 : set ⇒ apply_fun (q0 1) (q0 0)) q HqDom) (from left to right).
An exact proof term for the current goal is Hq1q0V.
An exact proof term for the current goal is (SepI Dom (λq0 : set ⇒ apply_fun (compact_open_evaluation_map X Tx Y Ty) q0 ∈ V) q HqDom Himgq).
∎