Assume Hex: ∃N : set, ∃e : set, N ∈ ω ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.

Apply Hex to the current goal.

Let N be given.

Assume HexN: ∃e : set, N ∈ ω ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.

Apply HexN to the current goal.

Let e be given.

Assume HNe: N ∈ ω ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.

We prove the intermediate claim HN: N ∈ ω.

An exact proof term for the current goal is (andEL (N ∈ ω) (embedding_of X Tx (euclidean_space N) (euclidean_topology N) e) HNe).

We prove the intermediate claim Hemb: embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.

An exact proof term for the current goal is (andER (N ∈ ω) (embedding_of X Tx (euclidean_space N) (euclidean_topology N) e) HNe).

Set EN to be the term euclidean_space N.

Set TN to be the term euclidean_topology N.

Set Im to be the term image_of e X.

Set Tim to be the term subspace_topology EN TN Im.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (compact_space_topology X Tx Hcomp).

We prove the intermediate claim Hcont: continuous_map X Tx EN TN e.

An exact proof term for the current goal is (embedding_of_continuous X Tx EN TN e Hemb).

We prove the intermediate claim Hfun: function_on e X EN.

An exact proof term for the current goal is (continuous_map_function_on X Tx EN TN e Hcont).

We prove the intermediate claim HImSubEN: Im ⊆ EN.

An exact proof term for the current goal is (image_of_sub_codomain e X EN X Hfun (Subq_ref X)).

We prove the intermediate claim HcompIm: compact_space Im Tim.

An exact proof term for the current goal is (continuous_image_compact X Tx EN TN e Hcomp Hcont).

We prove the intermediate claim HdimIm: covering_dimension Im Tim N.

An exact proof term for the current goal is (compact_subspace_RN_dimension_le_N Im N HN HImSubEN HcompIm).

We prove the intermediate claim Hhom: homeomorphism X Tx Im Tim e.

An exact proof term for the current goal is (embedding_of_homeomorphism X Tx EN TN e Hemb).

We prove the intermediate claim Hexg: ∃g : set, continuous_map Im Tim X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun e x) = x) ∧ (∀y : set, y ∈ Im → apply_fun e (apply_fun g y) = y).

An exact proof term for the current goal is (homeomorphism_inverse_package X Tx Im Tim e Hhom).

We prove the intermediate claim HdimX: covering_dimension X Tx N.

Apply (covering_dimensionI X Tx N) to the current goal.

An exact proof term for the current goal is HTx.

An exact proof term for the current goal is HN.

Let A be given.

Assume HA: open_cover_of X Tx A.

Apply Hexg to the current goal.

Let g be given.

Assume Hgpack: continuous_map Im Tim X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun e x) = x) ∧ (∀y : set, y ∈ Im → apply_fun e (apply_fun g y) = y).

We prove the intermediate claim Hg1: continuous_map Im Tim X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun e x) = x).

An exact proof term for the current goal is (andEL (continuous_map Im Tim X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun e x) = x)) (∀y : set, y ∈ Im → apply_fun e (apply_fun g y) = y) Hgpack).

We prove the intermediate claim Hgcont: continuous_map Im Tim X Tx g.

An exact proof term for the current goal is (andEL (continuous_map Im Tim X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun e x) = x) Hg1).

We prove the intermediate claim Hgf: ∀x : set, x ∈ X → apply_fun g (apply_fun e x) = x.

An exact proof term for the current goal is (andER (continuous_map Im Tim X Tx g) (∀x : set, x ∈ X → apply_fun g (apply_fun e x) = x) Hg1).

We prove the intermediate claim Hfg: ∀y : set, y ∈ Im → apply_fun e (apply_fun g y) = y.

An exact proof term for the current goal is (andER (continuous_map Im Tim X Tx g ∧ (∀x : set, x ∈ X → apply_fun g (apply_fun e x) = x)) (∀y : set, y ∈ Im → apply_fun e (apply_fun g y) = y) Hgpack).

Set Ag to be the term {preimage_of Im g U|U ∈ A}.

We prove the intermediate claim Hag_open: ∀U : set, U ∈ A → preimage_of Im g U ∈ Tim.

Let U be given.

Assume HUA: U ∈ A.

We prove the intermediate claim HUopen: U ∈ Tx.

We prove the intermediate claim Hmem: ∀W : set, W ∈ A → W ∈ Tx.

We prove the intermediate claim H0: ((topology_on X Tx ∧ A ⊆ 𝒫 X) ∧ X ⊆ ⋃ A) ∧ (∀W : set, W ∈ A → W ∈ Tx).

An exact proof term for the current goal is HA.

An exact proof term for the current goal is (andER ((topology_on X Tx ∧ A ⊆ 𝒫 X) ∧ X ⊆ ⋃ A) (∀W : set, W ∈ A → W ∈ Tx) H0).

An exact proof term for the current goal is (Hmem U HUA).

An exact proof term for the current goal is (continuous_map_preimage Im Tim X Tx g Hgcont U HUopen).

We prove the intermediate claim Hag: open_cover_of Im Tim Ag.

Apply (open_cover_ofI Im Tim Ag) to the current goal.

An exact proof term for the current goal is (covering_dimension_topology_on Im Tim N HdimIm).

Let V be given.

Assume HV: V ∈ Ag.

We will prove V ∈ 𝒫 Im.

Apply (ReplE_impred A (λU0 : set ⇒ preimage_of Im g U0) V HV) to the current goal.

Let U be given.

Assume HUA: U ∈ A.

Assume HVU: V = preimage_of Im g U.

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

We prove the intermediate claim Hsub: preimage_of Im g U ⊆ Im.

Let y be given.

Assume Hy: y ∈ preimage_of Im g U.

An exact proof term for the current goal is (SepE1 Im (λy0 : set ⇒ apply_fun g y0 ∈ U) y Hy).

An exact proof term for the current goal is (PowerI Im (preimage_of Im g U) Hsub).

Let y be given.

Assume HyIm: y ∈ Im.

We will prove y ∈ ⋃ Ag.

We prove the intermediate claim HgyX: apply_fun g y ∈ X.

We prove the intermediate claim Hgfun: function_on g Im X.

An exact proof term for the current goal is (continuous_map_function_on Im Tim X Tx g Hgcont).

An exact proof term for the current goal is (Hgfun y HyIm).

We prove the intermediate claim HcovX: X ⊆ ⋃ A.

An exact proof term for the current goal is (open_cover_of_covers X Tx A HA).

We prove the intermediate claim HgyUA: apply_fun g y ∈ ⋃ A.

An exact proof term for the current goal is (HcovX (apply_fun g y) HgyX).

Apply (UnionE_impred A (apply_fun g y) HgyUA) to the current goal.

Let U be given.

Assume HgyU: apply_fun g y ∈ U.

Assume HUA: U ∈ A.

We prove the intermediate claim HyPre: y ∈ preimage_of Im g U.

An exact proof term for the current goal is (SepI Im (λy0 : set ⇒ apply_fun g y0 ∈ U) y HyIm HgyU).

An exact proof term for the current goal is (UnionI Ag y (preimage_of Im g U) HyPre (ReplI A (λU0 : set ⇒ preimage_of Im g U0) U HUA)).

Let V be given.

Assume HV: V ∈ Ag.

Apply (ReplE_impred A (λU0 : set ⇒ preimage_of Im g U0) V HV) to the current goal.

Let U be given.

Assume HUA: U ∈ A.

Assume HVU: V = preimage_of Im g U.

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

An exact proof term for the current goal is (Hag_open U HUA).

We prove the intermediate claim HdimImprop: ∀A0 : set, open_cover_of Im Tim A0 → ∃B0 : set, open_cover_of Im Tim B0 ∧ refines_cover B0 A0 ∧ collection_has_order_at_most_m_plus_one Im B0 N.

An exact proof term for the current goal is (andER (topology_on Im Tim ∧ N ∈ ω) (∀A0 : set, open_cover_of Im Tim A0 → ∃B0 : set, open_cover_of Im Tim B0 ∧ refines_cover B0 A0 ∧ collection_has_order_at_most_m_plus_one Im B0 N) HdimIm).

We prove the intermediate claim HexB: ∃B : set, open_cover_of Im Tim B ∧ refines_cover B Ag ∧ collection_has_order_at_most_m_plus_one Im B N.

An exact proof term for the current goal is (HdimImprop Ag Hag).

Apply HexB to the current goal.

Let B be given.

Assume HBpack: open_cover_of Im Tim B ∧ refines_cover B Ag ∧ collection_has_order_at_most_m_plus_one Im B N.

We prove the intermediate claim HB1: open_cover_of Im Tim B ∧ refines_cover B Ag.

An exact proof term for the current goal is (andEL (open_cover_of Im Tim B ∧ refines_cover B Ag) (collection_has_order_at_most_m_plus_one Im B N) HBpack).

We prove the intermediate claim HBcover: open_cover_of Im Tim B.

An exact proof term for the current goal is (andEL (open_cover_of Im Tim B) (refines_cover B Ag) HB1).

We prove the intermediate claim HBref: refines_cover B Ag.

An exact proof term for the current goal is (andER (open_cover_of Im Tim B) (refines_cover B Ag) HB1).

We prove the intermediate claim HBorder: collection_has_order_at_most_m_plus_one Im B N.

An exact proof term for the current goal is (andER (open_cover_of Im Tim B ∧ refines_cover B Ag) (collection_has_order_at_most_m_plus_one Im B N) HBpack).

Set Be to be the term {preimage_of X e V|V ∈ B}.

We use Be to witness the existential quantifier.

Apply andI to the current goal.

Apply (open_cover_ofI X Tx Be) to the current goal.

An exact proof term for the current goal is HTx.

Let W be given.

Assume HW: W ∈ Be.

We will prove W ∈ 𝒫 X.

Apply (ReplE_impred B (λV0 : set ⇒ preimage_of X e V0) W HW) to the current goal.

Let V be given.

Assume HVB: V ∈ B.

Assume HWV: W = preimage_of X e V.

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

We prove the intermediate claim Hsub: preimage_of X e V ⊆ X.

Let x be given.

Assume Hx: x ∈ preimage_of X e V.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun e x0 ∈ V) x Hx).

An exact proof term for the current goal is (PowerI X (preimage_of X e V) Hsub).

Let x be given.

Assume HxX: x ∈ X.

We will prove x ∈ ⋃ Be.

We prove the intermediate claim HyIm: apply_fun e x ∈ Im.

An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ apply_fun e x0) x HxX).

We prove the intermediate claim HcovIm: Im ⊆ ⋃ B.

An exact proof term for the current goal is (open_cover_of_covers Im Tim B HBcover).

We prove the intermediate claim HyUB: apply_fun e x ∈ ⋃ B.

An exact proof term for the current goal is (HcovIm (apply_fun e x) HyIm).

Apply (UnionE_impred B (apply_fun e x) HyUB) to the current goal.

Let V be given.

Assume HyV: apply_fun e x ∈ V.

Assume HVB: V ∈ B.

We prove the intermediate claim HxPre: x ∈ preimage_of X e V.

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun e x0 ∈ V) x HxX HyV).

An exact proof term for the current goal is (UnionI Be x (preimage_of X e V) HxPre (ReplI B (λV0 : set ⇒ preimage_of X e V0) V HVB)).

Let W be given.

Assume HW: W ∈ Be.

Apply (ReplE_impred B (λV0 : set ⇒ preimage_of X e V0) W HW) to the current goal.

Let V be given.

Assume HVB: V ∈ B.

Assume HWV: W = preimage_of X e V.

We prove the intermediate claim HVopen: V ∈ Tim.

We prove the intermediate claim HmemB: ∀U : set, U ∈ B → U ∈ Tim.

We prove the intermediate claim H0: ((topology_on Im Tim ∧ B ⊆ 𝒫 Im) ∧ Im ⊆ ⋃ B) ∧ (∀U : set, U ∈ B → U ∈ Tim).

An exact proof term for the current goal is HBcover.

An exact proof term for the current goal is (andER ((topology_on Im Tim ∧ B ⊆ 𝒫 Im) ∧ Im ⊆ ⋃ B) (∀U : set, U ∈ B → U ∈ Tim) H0).

An exact proof term for the current goal is (HmemB V HVB).

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

An exact proof term for the current goal is (continuous_map_preimage X Tx Im Tim e (homeomorphism_continuous X Tx Im Tim e Hhom) V HVopen).

Let W be given.

Assume HW: W ∈ Be.

Apply (ReplE_impred B (λV0 : set ⇒ preimage_of X e V0) W HW) to the current goal.

Let V be given.

Assume HVB: V ∈ B.

Assume HWV: W = preimage_of X e V.

We prove the intermediate claim HexAg: ∃W0 : set, W0 ∈ Ag ∧ V ⊆ W0.

An exact proof term for the current goal is (HBref V HVB).

Apply HexAg to the current goal.

Let W0 be given.

Assume HW0pack: W0 ∈ Ag ∧ V ⊆ W0.

We prove the intermediate claim HW0Ag: W0 ∈ Ag.

An exact proof term for the current goal is (andEL (W0 ∈ Ag) (V ⊆ W0) HW0pack).

We prove the intermediate claim HVW0: V ⊆ W0.

An exact proof term for the current goal is (andER (W0 ∈ Ag) (V ⊆ W0) HW0pack).

Apply (ReplE_impred A (λU0 : set ⇒ preimage_of Im g U0) W0 HW0Ag) to the current goal.

Let U be given.

Assume HUA: U ∈ A.

Assume HW0U: W0 = preimage_of Im g U.

We use U to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HUA.

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

Let x be given.

Assume HxPre: x ∈ preimage_of X e V.

We will prove x ∈ U.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ apply_fun e x0 ∈ V) x HxPre).

We prove the intermediate claim HyV: apply_fun e x ∈ V.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun e x0 ∈ V) x HxPre).

We prove the intermediate claim HyW0: apply_fun e x ∈ W0.

An exact proof term for the current goal is (HVW0 (apply_fun e x) HyV).

We prove the intermediate claim HyPreU: apply_fun e x ∈ preimage_of Im g U.

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

An exact proof term for the current goal is HyW0.

We prove the intermediate claim HgyU: apply_fun g (apply_fun e x) ∈ U.

An exact proof term for the current goal is (SepE2 Im (λy0 : set ⇒ apply_fun g y0 ∈ U) (apply_fun e x) HyPreU).

We prove the intermediate claim Hgx: apply_fun g (apply_fun e x) = x.

An exact proof term for the current goal is (Hgf x HxX).

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

An exact proof term for the current goal is HgyU.

We will prove collection_has_order_at_most_m_plus_one X Be N.

We will prove ordinal N ∧ ∀x : set, x ∈ X → cardinality_at_most {U ∈ Be|x ∈ U} (ordsucc N).

Apply andI to the current goal.

An exact proof term for the current goal is (ordinal_Hered ω omega_ordinal N HN).

Let x be given.

Assume HxX: x ∈ X.

We prove the intermediate claim HyIm: apply_fun e x ∈ Im.

An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ apply_fun e x0) x HxX).

We prove the intermediate claim HordCore: ordinal N ∧ ∀y : set, y ∈ Im → cardinality_at_most {U ∈ B|y ∈ U} (ordsucc N).

An exact proof term for the current goal is HBorder.

We prove the intermediate claim HcardY: cardinality_at_most {U ∈ B|apply_fun e x ∈ U} (ordsucc N).

An exact proof term for the current goal is ((andER (ordinal N) (∀y : set, y ∈ Im → cardinality_at_most {U ∈ B|y ∈ U} (ordsucc N)) HordCore) (apply_fun e x) HyIm).

Set S to be the term {U ∈ B|apply_fun e x ∈ U}.

We prove the intermediate claim Heq: {W ∈ Be|x ∈ W} = {preimage_of X e U|U ∈ S}.

Apply set_ext to the current goal.

Let W be given.

Assume HW: W ∈ {W0 ∈ Be|x ∈ W0}.

We prove the intermediate claim HWBe: W ∈ Be.

An exact proof term for the current goal is (SepE1 Be (λW0 : set ⇒ x ∈ W0) W HW).

We prove the intermediate claim HxW: x ∈ W.

An exact proof term for the current goal is (SepE2 Be (λW0 : set ⇒ x ∈ W0) W HW).

Apply (ReplE_impred B (λU0 : set ⇒ preimage_of X e U0) W HWBe) to the current goal.

Let U be given.

Assume HUB: U ∈ B.

Assume HWU: W = preimage_of X e U.

We prove the intermediate claim HyU: apply_fun e x ∈ U.

We prove the intermediate claim HxPreU: x ∈ preimage_of X e U.

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

An exact proof term for the current goal is HxW.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ apply_fun e x0 ∈ U) x HxPreU).

We prove the intermediate claim HUS: U ∈ S.

Apply SepI to the current goal.

An exact proof term for the current goal is HUB.

An exact proof term for the current goal is HyU.

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

An exact proof term for the current goal is (ReplI S (λU0 : set ⇒ preimage_of X e U0) U HUS).

Let W be given.

Assume HW: W ∈ {preimage_of X e U|U ∈ S}.

Apply (ReplE_impred S (λU0 : set ⇒ preimage_of X e U0) W HW) to the current goal.

Let U be given.

Assume HUS: U ∈ S.

Assume HWU: W = preimage_of X e U.

We prove the intermediate claim HUB: U ∈ B.

An exact proof term for the current goal is (SepE1 B (λU0 : set ⇒ apply_fun e x ∈ U0) U HUS).

We prove the intermediate claim HyU: apply_fun e x ∈ U.

An exact proof term for the current goal is (SepE2 B (λU0 : set ⇒ apply_fun e x ∈ U0) U HUS).

We prove the intermediate claim HWBe: W ∈ Be.

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

An exact proof term for the current goal is (ReplI B (λU0 : set ⇒ preimage_of X e U0) U HUB).

We prove the intermediate claim HxPre: x ∈ preimage_of X e U.

An exact proof term for the current goal is (SepI X (λx0 : set ⇒ apply_fun e x0 ∈ U) x HxX HyU).

Apply SepI to the current goal.

An exact proof term for the current goal is HWBe.

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

An exact proof term for the current goal is HxPre.

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

An exact proof term for the current goal is (cardinality_at_most_image_finite S N (λU0 : set ⇒ preimage_of X e U0) HN HcardY).

An exact proof term for the current goal is (covering_dimension_implies_finite_dimensional_space X Tx N HdimX).

Assume Hfd: finite_dimensional_space X Tx.

We prove the intermediate claim Hexm: ∃m : set, covering_dimension X Tx m.

An exact proof term for the current goal is (finite_dimensional_space_implies_exists_covering_dimension X Tx Hfd).

Apply Hexm to the current goal.

Let m be given.

Assume Hdim: covering_dimension X Tx m.

We prove the intermediate claim HmO: m ∈ ω.

An exact proof term for the current goal is (covering_dimension_n_in_omega X Tx m Hdim).

We prove the intermediate claim HexEmb: ∃N : set, ∃e : set, N = add_nat (mul_nat two m) (Sing Empty) ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.

An exact proof term for the current goal is (Menger_Nobeling_embedding_full X Tx m Hcomp Hmet Hdim HmO).

Apply HexEmb to the current goal.

Let N be given.

Assume Hexe: ∃e : set, N = add_nat (mul_nat two m) (Sing Empty) ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.

Apply Hexe to the current goal.

Let e be given.

Assume HNe: N = add_nat (mul_nat two m) (Sing Empty) ∧ embedding_of X Tx (euclidean_space N) (euclidean_topology N) e.

We use N to witness the existential quantifier.

We use e to witness the existential quantifier.

Apply andI to the current goal.

We prove the intermediate claim HNeq: N = add_nat (mul_nat two m) (Sing Empty).

An exact proof term for the current goal is (andEL (N = add_nat (mul_nat two m) (Sing Empty)) (embedding_of X Tx (euclidean_space N) (euclidean_topology N) e) HNe).

We prove the intermediate claim HmNat: nat_p m.

An exact proof term for the current goal is (omega_nat_p m HmO).

We prove the intermediate claim HtwoEq: two = 2.

Use reflexivity.

We prove the intermediate claim HtwoNat: nat_p two.

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

An exact proof term for the current goal is nat_2.

We prove the intermediate claim HoneEq: (Sing Empty) = 1.

We prove the intermediate claim Hsucc0eq1: ordsucc 0 = 1.

Use reflexivity.

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

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ (Sing Empty).

We prove the intermediate claim HxeqE: x = Empty.

An exact proof term for the current goal is (SingE Empty x Hx).

We prove the intermediate claim H0EqE: 0 = Empty.

Use reflexivity.

We prove the intermediate claim Hxeq0: x = 0.

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

An exact proof term for the current goal is HxeqE.

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

An exact proof term for the current goal is (ordsuccI2 0).

Let x be given.

Assume Hx: x ∈ ordsucc 0.

Apply (ordsuccE 0 x Hx (x ∈ Sing Empty)) to the current goal.

Assume Hx0: x ∈ 0.

Apply FalseE to the current goal.

An exact proof term for the current goal is ((EmptyE x) Hx0).

Assume Hxeq0: x = 0.

We prove the intermediate claim H0EqE: 0 = Empty.

Use reflexivity.

We prove the intermediate claim HxeqE: x = Empty.

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

An exact proof term for the current goal is Hxeq0.

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

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

We prove the intermediate claim HoneNat: nat_p (Sing Empty).

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

An exact proof term for the current goal is nat_1.

We prove the intermediate claim HtwoO: two ∈ ω.

An exact proof term for the current goal is (nat_p_omega two HtwoNat).

We prove the intermediate claim HmulNat: nat_p (mul_nat two m).

An exact proof term for the current goal is (mul_nat_p two HtwoNat m HmNat).

We prove the intermediate claim HmulO: (mul_nat two m) ∈ ω.

An exact proof term for the current goal is (nat_p_omega (mul_nat two m) HmulNat).

We prove the intermediate claim HoneO: (Sing Empty) ∈ ω.

An exact proof term for the current goal is (nat_p_omega (Sing Empty) HoneNat).

We prove the intermediate claim HaddNat: nat_p (add_nat (mul_nat two m) (Sing Empty)).

An exact proof term for the current goal is (add_nat_p (mul_nat two m) HmulNat (Sing Empty) HoneNat).

We prove the intermediate claim HNatN: nat_p N.

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

An exact proof term for the current goal is HaddNat.

An exact proof term for the current goal is (nat_p_omega N HNatN).

An exact proof term for the current goal is (andER (N = add_nat (mul_nat two m) (Sing Empty)) (embedding_of X Tx (euclidean_space N) (euclidean_topology N) e) HNe).