Let y be given.

Assume HyU: y ∈ space_family_union I (const_space_family I X Tx).

We will prove y ∈ X.

We prove the intermediate claim Hdef: space_family_union I (const_space_family I X Tx) = ⋃ {space_family_set (const_space_family I X Tx) i|i ∈ I}.

Use reflexivity.

We prove the intermediate claim HyU': y ∈ ⋃ {space_family_set (const_space_family I X Tx) i|i ∈ I}.

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

An exact proof term for the current goal is HyU.

Apply (UnionE_impred {space_family_set (const_space_family I X Tx) i|i ∈ I} y HyU') to the current goal.

Let A be given.

Assume HyA: y ∈ A.

Assume HA: A ∈ {space_family_set (const_space_family I X Tx) i|i ∈ I}.

Apply (ReplE_impred I (λi0 : set ⇒ space_family_set (const_space_family I X Tx) i0) A HA (y ∈ X)) to the current goal.

Let i be given.

Assume HiI: i ∈ I.

Assume HAeq: A = space_family_set (const_space_family I X Tx) i.

We prove the intermediate claim HyAi: y ∈ space_family_set (const_space_family I X Tx) i.

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

An exact proof term for the current goal is HyA.

rewrite the current goal using (space_family_set_const_space_family I X Tx i HiI) (from right to left).

An exact proof term for the current goal is HyAi.

Let y be given.

Assume HyX: y ∈ X.

We will prove y ∈ space_family_union I (const_space_family I X Tx).

We prove the intermediate claim Hexi0: ∃i0 : set, i0 ∈ I.

Apply (xm (∃i0 : set, i0 ∈ I)) to the current goal.

Assume Hex.

An exact proof term for the current goal is Hex.

Assume Hno: ¬ (∃i0 : set, i0 ∈ I).

Apply FalseE to the current goal.

We prove the intermediate claim Hsub0: I ⊆ Empty.

Let i be given.

Assume HiI: i ∈ I.

We will prove i ∈ Empty.

Apply FalseE to the current goal.

We will prove False.

Apply Hno to the current goal.

We use i to witness the existential quantifier.

An exact proof term for the current goal is HiI.

We prove the intermediate claim HI0: I = Empty.

An exact proof term for the current goal is (Empty_Subq_eq I Hsub0).

An exact proof term for the current goal is (HIne HI0).

Apply Hexi0 to the current goal.

Let i0 be given.

Assume Hi0I: i0 ∈ I.

Set A0 to be the term space_family_set (const_space_family I X Tx) i0.

We prove the intermediate claim HA0fam: A0 ∈ {space_family_set (const_space_family I X Tx) i|i ∈ I}.

An exact proof term for the current goal is (ReplI I (λi : set ⇒ space_family_set (const_space_family I X Tx) i) i0 Hi0I).

We prove the intermediate claim HyA0: y ∈ A0.

We prove the intermediate claim HA0def: A0 = space_family_set (const_space_family I X Tx) i0.

Use reflexivity.

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

rewrite the current goal using (space_family_set_const_space_family I X Tx i0 Hi0I) (from left to right).

An exact proof term for the current goal is HyX.

We prove the intermediate claim Hdef: space_family_union I (const_space_family I X Tx) = ⋃ {space_family_set (const_space_family I X Tx) i|i ∈ I}.

Use reflexivity.

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

An exact proof term for the current goal is (UnionI {space_family_set (const_space_family I X Tx) i|i ∈ I} y A0 HyA0 HA0fam).