We will prove topology_on X Tx ∧ ∀A : set, A ⊆ X → infinite A → ∃x : set, limit_point_of X Tx A x.

Apply andI to the current goal.

An exact proof term for the current goal is (product_topology_is_topology ω Tx0 Y Ty (discrete_topology_on ω) (indiscrete_topology_on Y)).

Let A be given.

Assume HA: A ⊆ X.

Assume HinfA: infinite A.

We will prove ∃x : set, limit_point_of X Tx A x.

We prove the intermediate claim HAnotEmpty: A ≠ Empty.

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

Assume HAeq: A = Empty.

Apply FalseE to the current goal.

We will prove False.

Apply HinfA to the current goal.

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

An exact proof term for the current goal is finite_Empty.

Assume Hneq: A ≠ Empty.

An exact proof term for the current goal is Hneq.

We prove the intermediate claim Hexa: ∃a : set, a ∈ A.

Apply (xm (∃a : set, a ∈ A)) to the current goal.

Assume Hex.

An exact proof term for the current goal is Hex.

Assume Hnoex: ¬ (∃a : set, a ∈ A).

Apply FalseE to the current goal.

We will prove False.

Apply HAnotEmpty to the current goal.

Apply set_ext to the current goal.

Let x be given.

Assume HxA: x ∈ A.

Apply FalseE to the current goal.

We will prove False.

We prove the intermediate claim Hex: ∃a : set, a ∈ A.

We use x to witness the existential quantifier.

An exact proof term for the current goal is HxA.

An exact proof term for the current goal is (Hnoex Hex).

Let x be given.

Assume HxE: x ∈ Empty.

Apply FalseE to the current goal.

We will prove False.

Apply (EmptyE x) to the current goal.

An exact proof term for the current goal is HxE.

Apply Hexa to the current goal.

Let a be given.

Assume HaA: a ∈ A.

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (HA a HaA).

We prove the intermediate claim Ha0w: a 0 ∈ ω.

An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ Y) a HaX).

We prove the intermediate claim Ha1Y: a 1 ∈ Y.

An exact proof term for the current goal is (ap1_Sigma ω (λ_ : set ⇒ Y) a HaX).

We prove the intermediate claim Ha1cases: a 1 = 0 ∨ a 1 = 1.

An exact proof term for the current goal is (UPairE (a 1) 0 1 Ha1Y).

Apply Ha1cases to the current goal.

Assume Ha10: a 1 = 0.

Set x to be the term (a 0,1).

We use x to witness the existential quantifier.

We will prove limit_point_of X Tx A x.

We will prove topology_on X Tx ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.

Apply andI to the current goal.

An exact proof term for the current goal is (product_topology_is_topology ω Tx0 Y Ty (discrete_topology_on ω) (indiscrete_topology_on Y)).

We prove the intermediate claim H1Y: 1 ∈ Y.

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω Y (a 0) 1 Ha0w H1Y).

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We will prove ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.

We prove the intermediate claim HUprop: ∀p ∈ U, ∃b ∈ product_subbasis ω Tx0 Y Ty, p ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀p0 ∈ U0, ∃b ∈ product_subbasis ω Tx0 Y Ty, p0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim Hexb: ∃b ∈ product_subbasis ω Tx0 Y Ty, x ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (HUprop x HxU).

Apply Hexb to the current goal.

Let b be given.

Assume Hbp: b ∈ product_subbasis ω Tx0 Y Ty ∧ (x ∈ b ∧ b ⊆ U).

We prove the intermediate claim HbB: b ∈ product_subbasis ω Tx0 Y Ty.

An exact proof term for the current goal is (andEL (b ∈ product_subbasis ω Tx0 Y Ty) (x ∈ b ∧ b ⊆ U) Hbp).

We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (andER (b ∈ product_subbasis ω Tx0 Y Ty) (x ∈ b ∧ b ⊆ U) Hbp).

We prove the intermediate claim Hxb: x ∈ b.

An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim HbsubU: b ⊆ U.

An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim HexU0: ∃U0 ∈ Tx0, b ∈ {rectangle_set U0 V|V ∈ Ty}.

An exact proof term for the current goal is (famunionE Tx0 (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b HbB).

Apply HexU0 to the current goal.

Let U0 be given.

Assume HU0pair: U0 ∈ Tx0 ∧ b ∈ {rectangle_set U0 V|V ∈ Ty}.

We prove the intermediate claim HU0: U0 ∈ Tx0.

An exact proof term for the current goal is (andEL (U0 ∈ Tx0) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0pair).

We prove the intermediate claim HbRepl: b ∈ {rectangle_set U0 V|V ∈ Ty}.

An exact proof term for the current goal is (andER (U0 ∈ Tx0) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0pair).

We prove the intermediate claim HexV0: ∃V0 ∈ Ty, b = rectangle_set U0 V0.

An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U0 V0) b HbRepl).

Apply HexV0 to the current goal.

Let V0 be given.

Assume HV0pair: V0 ∈ Ty ∧ b = rectangle_set U0 V0.

We prove the intermediate claim HV0: V0 ∈ Ty.

An exact proof term for the current goal is (andEL (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0pair).

We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.

An exact proof term for the current goal is (andER (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0pair).

We prove the intermediate claim HxRect: x ∈ rectangle_set U0 V0.

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

An exact proof term for the current goal is Hxb.

We prove the intermediate claim Hx0U0: x 0 ∈ U0.

An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) x HxRect).

We prove the intermediate claim Hx1V0: x 1 ∈ V0.

An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) x HxRect).

We prove the intermediate claim Hx0eq: x 0 = a 0.

An exact proof term for the current goal is (tuple_2_0_eq (a 0) 1).

We prove the intermediate claim Hx1eq: x 1 = 1.

An exact proof term for the current goal is (tuple_2_1_eq (a 0) 1).

We prove the intermediate claim Ha0U0: a 0 ∈ U0.

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

An exact proof term for the current goal is Hx0U0.

We prove the intermediate claim HV0cases: V0 = Empty ∨ V0 = Y.

An exact proof term for the current goal is (UPairE V0 Empty Y HV0).

We prove the intermediate claim HV0ne: V0 ≠ Empty.

An exact proof term for the current goal is (elem_implies_nonempty V0 (x 1) Hx1V0).

We prove the intermediate claim HV0Y: V0 = Y.

Apply HV0cases to the current goal.

Assume HV0E: V0 = Empty.

Apply FalseE to the current goal.

We will prove False.

An exact proof term for the current goal is (HV0ne HV0E).

Assume HV0Y': V0 = Y.

An exact proof term for the current goal is HV0Y'.

We prove the intermediate claim HxRectY: x ∈ rectangle_set U0 Y.

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

An exact proof term for the current goal is HxRect.

We prove the intermediate claim HaEta: a = (a 0,a 1).

An exact proof term for the current goal is (setprod_eta ω Y a HaX).

We prove the intermediate claim H0Y: 0 ∈ Y.

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

We prove the intermediate claim HaInRect: a ∈ rectangle_set U0 V0.

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

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

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U0 Y (a 0) 0 Ha0U0 H0Y).

We prove the intermediate claim HaInb: a ∈ b.

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

An exact proof term for the current goal is HaInRect.

We prove the intermediate claim HaU: a ∈ U.

An exact proof term for the current goal is (HbsubU a HaInb).

We use a to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaA.

We will prove a ≠ x.

Assume Heq: a = x.

We prove the intermediate claim Heq1: a 1 = x 1.

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

Use reflexivity.

We prove the intermediate claim H01: 0 = 1.

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

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

An exact proof term for the current goal is Heq1.

An exact proof term for the current goal is (neq_0_1 H01).

An exact proof term for the current goal is HaU.

Assume Ha11: a 1 = 1.

Set x to be the term (a 0,0).

We use x to witness the existential quantifier.

We will prove limit_point_of X Tx A x.

We will prove topology_on X Tx ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.

Apply andI to the current goal.

An exact proof term for the current goal is (product_topology_is_topology ω Tx0 Y Ty (discrete_topology_on ω) (indiscrete_topology_on Y)).

We prove the intermediate claim H0Y: 0 ∈ Y.

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω Y (a 0) 0 Ha0w H0Y).

Let U be given.

Assume HU: U ∈ Tx.

Assume HxU: x ∈ U.

We will prove ∃y : set, y ∈ A ∧ y ≠ x ∧ y ∈ U.

We prove the intermediate claim HUprop: ∀p ∈ U, ∃b ∈ product_subbasis ω Tx0 Y Ty, p ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀p0 ∈ U0, ∃b ∈ product_subbasis ω Tx0 Y Ty, p0 ∈ b ∧ b ⊆ U0) U HU).

We prove the intermediate claim Hexb: ∃b ∈ product_subbasis ω Tx0 Y Ty, x ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (HUprop x HxU).

Apply Hexb to the current goal.

Let b be given.

Assume Hbp: b ∈ product_subbasis ω Tx0 Y Ty ∧ (x ∈ b ∧ b ⊆ U).

We prove the intermediate claim HbB: b ∈ product_subbasis ω Tx0 Y Ty.

An exact proof term for the current goal is (andEL (b ∈ product_subbasis ω Tx0 Y Ty) (x ∈ b ∧ b ⊆ U) Hbp).

We prove the intermediate claim Hbprop: x ∈ b ∧ b ⊆ U.

An exact proof term for the current goal is (andER (b ∈ product_subbasis ω Tx0 Y Ty) (x ∈ b ∧ b ⊆ U) Hbp).

We prove the intermediate claim Hxb: x ∈ b.

An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim HbsubU: b ⊆ U.

An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ U) Hbprop).

We prove the intermediate claim HexU0: ∃U0 ∈ Tx0, b ∈ {rectangle_set U0 V|V ∈ Ty}.

An exact proof term for the current goal is (famunionE Tx0 (λU0 : set ⇒ {rectangle_set U0 V|V ∈ Ty}) b HbB).

Apply HexU0 to the current goal.

Let U0 be given.

Assume HU0pair: U0 ∈ Tx0 ∧ b ∈ {rectangle_set U0 V|V ∈ Ty}.

We prove the intermediate claim HbRepl: b ∈ {rectangle_set U0 V|V ∈ Ty}.

An exact proof term for the current goal is (andER (U0 ∈ Tx0) (b ∈ {rectangle_set U0 V|V ∈ Ty}) HU0pair).

We prove the intermediate claim HexV0: ∃V0 ∈ Ty, b = rectangle_set U0 V0.

An exact proof term for the current goal is (ReplE Ty (λV0 : set ⇒ rectangle_set U0 V0) b HbRepl).

Apply HexV0 to the current goal.

Let V0 be given.

Assume HV0pair: V0 ∈ Ty ∧ b = rectangle_set U0 V0.

We prove the intermediate claim HV0: V0 ∈ Ty.

An exact proof term for the current goal is (andEL (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0pair).

We prove the intermediate claim Hbeq: b = rectangle_set U0 V0.

An exact proof term for the current goal is (andER (V0 ∈ Ty) (b = rectangle_set U0 V0) HV0pair).

We prove the intermediate claim HxRect: x ∈ rectangle_set U0 V0.

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

An exact proof term for the current goal is Hxb.

We prove the intermediate claim Hx0U0: x 0 ∈ U0.

An exact proof term for the current goal is (ap0_Sigma U0 (λ_ : set ⇒ V0) x HxRect).

We prove the intermediate claim Hx1V0: x 1 ∈ V0.

An exact proof term for the current goal is (ap1_Sigma U0 (λ_ : set ⇒ V0) x HxRect).

We prove the intermediate claim Hx0eq: x 0 = a 0.

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

We prove the intermediate claim Hx1eq: x 1 = 0.

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

We prove the intermediate claim Ha0U0: a 0 ∈ U0.

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

An exact proof term for the current goal is Hx0U0.

We prove the intermediate claim HV0cases: V0 = Empty ∨ V0 = Y.

An exact proof term for the current goal is (UPairE V0 Empty Y HV0).

We prove the intermediate claim HV0ne: V0 ≠ Empty.

An exact proof term for the current goal is (elem_implies_nonempty V0 (x 1) Hx1V0).

We prove the intermediate claim HV0Y: V0 = Y.

Apply HV0cases to the current goal.

Assume HV0E: V0 = Empty.

Apply FalseE to the current goal.

We will prove False.

An exact proof term for the current goal is (HV0ne HV0E).

Assume HV0Y': V0 = Y.

An exact proof term for the current goal is HV0Y'.

We prove the intermediate claim HaEta: a = (a 0,a 1).

An exact proof term for the current goal is (setprod_eta ω Y a HaX).

We prove the intermediate claim H1Y: 1 ∈ Y.

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

We prove the intermediate claim HaInRect: a ∈ rectangle_set U0 V0.

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

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

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

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma U0 Y (a 0) 1 Ha0U0 H1Y).

We prove the intermediate claim HaInb: a ∈ b.

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

An exact proof term for the current goal is HaInRect.

We prove the intermediate claim HaU: a ∈ U.

An exact proof term for the current goal is (HbsubU a HaInb).

We use a to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaA.

We will prove a ≠ x.

Assume Heq: a = x.

We prove the intermediate claim Heq1: a 1 = x 1.

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

Use reflexivity.

We prove the intermediate claim H01: 0 = 1.

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

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

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

Use reflexivity.

An exact proof term for the current goal is (neq_0_1 H01).

An exact proof term for the current goal is HaU.

We will prove ¬ compact_space X Tx.

Assume Hcomp: compact_space X Tx.

Set Fam to be the term {rectangle_set {n} Y|n ∈ ω}.

We prove the intermediate claim Hcov: open_cover_of X Tx Fam.

We will prove topology_on X Tx ∧ Fam ⊆ 𝒫 X ∧ X ⊆ ⋃ Fam ∧ (∀U0 : set, U0 ∈ Fam → U0 ∈ Tx).

Apply andI to the current goal.

An exact proof term for the current goal is (product_topology_is_topology ω Tx0 Y Ty (discrete_topology_on ω) (indiscrete_topology_on Y)).

Let U0 be given.

Assume HU0: U0 ∈ Fam.

We will prove U0 ∈ 𝒫 X.

Apply (ReplE ω (λn : set ⇒ rectangle_set {n} Y) U0 HU0) to the current goal.

Let n be given.

Assume Hnconj: n ∈ ω ∧ U0 = rectangle_set {n} Y.

We prove the intermediate claim Hn: n ∈ ω.

An exact proof term for the current goal is (andEL (n ∈ ω) (U0 = rectangle_set {n} Y) Hnconj).

We prove the intermediate claim HU0eq: U0 = rectangle_set {n} Y.

An exact proof term for the current goal is (andER (n ∈ ω) (U0 = rectangle_set {n} Y) Hnconj).

We prove the intermediate claim HsingSub: {n} ⊆ ω.

An exact proof term for the current goal is (singleton_subset n ω Hn).

We prove the intermediate claim HrectSub: rectangle_set {n} Y ⊆ X.

An exact proof term for the current goal is (setprod_Subq {n} Y ω Y HsingSub (Subq_ref Y)).

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

An exact proof term for the current goal is (PowerI X (rectangle_set {n} Y) HrectSub).

Let p be given.

Assume HpX: p ∈ X.

We will prove p ∈ ⋃ Fam.

We prove the intermediate claim Hp0w: p 0 ∈ ω.

An exact proof term for the current goal is (ap0_Sigma ω (λ_ : set ⇒ Y) p HpX).

We prove the intermediate claim Hp1Y: p 1 ∈ Y.

An exact proof term for the current goal is (ap1_Sigma ω (λ_ : set ⇒ Y) p HpX).

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

An exact proof term for the current goal is (setprod_eta ω Y p HpX).

We prove the intermediate claim HU0Fam: rectangle_set {p 0} Y ∈ Fam.

An exact proof term for the current goal is (ReplI ω (λn : set ⇒ rectangle_set {n} Y) (p 0) Hp0w).

We prove the intermediate claim HpU0: p ∈ rectangle_set {p 0} Y.

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

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

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

An exact proof term for the current goal is (tuple_2_rectangle_set {p 0} Y (p 0) (p 1) Hsing Hp1Y).

An exact proof term for the current goal is (UnionI Fam p (rectangle_set {p 0} Y) HpU0 HU0Fam).

Let U0 be given.

Assume HU0: U0 ∈ Fam.

We will prove U0 ∈ Tx.

Apply (ReplE ω (λn : set ⇒ rectangle_set {n} Y) U0 HU0) to the current goal.

Let n be given.

Assume Hnconj: n ∈ ω ∧ U0 = rectangle_set {n} Y.

We prove the intermediate claim Hn: n ∈ ω.

An exact proof term for the current goal is (andEL (n ∈ ω) (U0 = rectangle_set {n} Y) Hnconj).

We prove the intermediate claim HU0eq: U0 = rectangle_set {n} Y.

An exact proof term for the current goal is (andER (n ∈ ω) (U0 = rectangle_set {n} Y) Hnconj).

We prove the intermediate claim HTx0: topology_on ω Tx0.

An exact proof term for the current goal is (discrete_topology_on ω).

We prove the intermediate claim HTy: topology_on Y Ty.

An exact proof term for the current goal is (indiscrete_topology_on Y).

We prove the intermediate claim HBasis: basis_on X (product_subbasis ω Tx0 Y Ty).

An exact proof term for the current goal is (product_subbasis_is_basis ω Tx0 Y Ty HTx0 HTy).

We prove the intermediate claim HsingOpen: {n} ∈ Tx0.

Apply PowerI to the current goal.

An exact proof term for the current goal is (singleton_subset n ω Hn).

We prove the intermediate claim HYopen: Y ∈ Ty.

An exact proof term for the current goal is (topology_has_X Y Ty HTy).

We prove the intermediate claim HU0sub: rectangle_set {n} Y ∈ product_subbasis ω Tx0 Y Ty.

We prove the intermediate claim HrectFam: rectangle_set {n} Y ∈ {rectangle_set {n} V0|V0 ∈ Ty}.

An exact proof term for the current goal is (ReplI Ty (λV0 : set ⇒ rectangle_set {n} V0) Y HYopen).

An exact proof term for the current goal is (famunionI Tx0 (λU1 : set ⇒ {rectangle_set U1 V0|V0 ∈ Ty}) {n} (rectangle_set {n} Y) HsingOpen HrectFam).

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

An exact proof term for the current goal is (generated_topology_contains_basis X (product_subbasis ω Tx0 Y Ty) HBasis (rectangle_set {n} Y) HU0sub).

We prove the intermediate claim Hfin: has_finite_subcover X Tx Fam.

An exact proof term for the current goal is (compact_space_subcover_property X Tx Hcomp Fam Hcov).

Apply Hfin to the current goal.

Let G be given.

Assume HG: G ⊆ Fam ∧ finite G ∧ X ⊆ ⋃ G.

We prove the intermediate claim HGleft: G ⊆ Fam ∧ finite G.

An exact proof term for the current goal is (andEL (G ⊆ Fam ∧ finite G) (X ⊆ ⋃ G) HG).

We prove the intermediate claim HcovG: X ⊆ ⋃ G.

An exact proof term for the current goal is (andER (G ⊆ Fam ∧ finite G) (X ⊆ ⋃ G) HG).

We prove the intermediate claim HGsub: G ⊆ Fam.

An exact proof term for the current goal is (andEL (G ⊆ Fam) (finite G) HGleft).

We prove the intermediate claim HGfin: finite G.

An exact proof term for the current goal is (andER (G ⊆ Fam) (finite G) HGleft).

Set pickN to be the term λg : set ⇒ Eps_i (λn : set ⇒ n ∈ ω ∧ g = rectangle_set {n} Y).

Set N to be the term {pickN g|g ∈ G}.

We prove the intermediate claim HNfin: finite N.

An exact proof term for the current goal is (Repl_finite (λg : set ⇒ pickN g) G HGfin).

We prove the intermediate claim H0Y: 0 ∈ Y.

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

We prove the intermediate claim HomegaSub: ω ⊆ N.

Let m be given.

Assume Hm: m ∈ ω.

We will prove m ∈ N.

Set p to be the term (m,0).

We prove the intermediate claim HpX: p ∈ X.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω Y m 0 Hm H0Y).

We prove the intermediate claim HpUnion: p ∈ ⋃ G.

An exact proof term for the current goal is (HcovG p HpX).

Apply (UnionE_impred G p HpUnion) to the current goal.

Let g be given.

Assume Hpg: p ∈ g.

Assume HgG: g ∈ G.

We prove the intermediate claim HgFam: g ∈ Fam.

An exact proof term for the current goal is (HGsub g HgG).

We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ g = rectangle_set {n} Y.

An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ rectangle_set {n0} Y) g HgFam).

We prove the intermediate claim HpickProp: pickN g ∈ ω ∧ g = rectangle_set {pickN g} Y.

An exact proof term for the current goal is (Eps_i_ex (λn : set ⇒ n ∈ ω ∧ g = rectangle_set {n} Y) Hexn).

We prove the intermediate claim HgeqPick: g = rectangle_set {pickN g} Y.

An exact proof term for the current goal is (andER (pickN g ∈ ω) (g = rectangle_set {pickN g} Y) HpickProp).

We prove the intermediate claim HpInPickRect: p ∈ rectangle_set {pickN g} Y.

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

An exact proof term for the current goal is Hpg.

We prove the intermediate claim Hp0InSing: p 0 ∈ {pickN g}.

An exact proof term for the current goal is (ap0_Sigma {pickN g} (λ_ : set ⇒ Y) p HpInPickRect).

We prove the intermediate claim Hpeq0: p 0 = m.

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

We prove the intermediate claim HmInSing: m ∈ {pickN g}.

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

An exact proof term for the current goal is Hp0InSing.

We prove the intermediate claim HmEq: m = pickN g.

An exact proof term for the current goal is (SingE (pickN g) m HmInSing).

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

An exact proof term for the current goal is (ReplI G (λg0 : set ⇒ pickN g0) g HgG).

We prove the intermediate claim HfinOmega: finite ω.

An exact proof term for the current goal is (Subq_finite N HNfin ω HomegaSub).

We prove the intermediate claim HinfOmega: infinite ω.

We prove the intermediate claim Hatleast: atleastp ω ω.

An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).

An exact proof term for the current goal is (atleastp_omega_infinite ω Hatleast).

Apply FalseE to the current goal.

We will prove False.

An exact proof term for the current goal is (HinfOmega HfinOmega).