Let Fam be given.

Assume Hcover: open_cover_of X Tx Fam.

We will prove has_finite_subcover X Tx Fam.

We prove the intermediate claim HaX: a ∈ X.

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

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

We prove the intermediate claim Hcovsub: X ⊆ ⋃ Fam.

An exact proof term for the current goal is (open_cover_of_covers X Tx Fam Hcover).

We prove the intermediate claim HaUnion: a ∈ ⋃ Fam.

An exact proof term for the current goal is (Hcovsub a HaX).

Apply (UnionE_impred Fam a HaUnion (has_finite_subcover X Tx Fam)) to the current goal.

Let U be given.

Assume HaU: a ∈ U.

Assume HUfam: U ∈ Fam.

Apply (has_finite_subcoverI X Tx Fam {U}) to the current goal.

Apply andI to the current goal.

Let V be given.

Assume HV: V ∈ {U}.

We prove the intermediate claim HVe: V = U.

An exact proof term for the current goal is (SingE U V HV).

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

An exact proof term for the current goal is HUfam.

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

Let x be given.

Assume HxX: x ∈ X.

We will prove x ∈ ⋃ {U}.

We prove the intermediate claim HxS: x ∈ {a}.

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

An exact proof term for the current goal is HxX.

We prove the intermediate claim Hxa: x = a.

An exact proof term for the current goal is (SingE a x HxS).

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

An exact proof term for the current goal is (UnionI {U} a U HaU (SingI U)).