Let X, Tx, Fam and G be given.

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

We will prove has_finite_subcover X Tx Fam.

We will prove ∃G1 : set, G1 ⊆ Fam ∧ finite G1 ∧ X ⊆ ⋃ G1.

We use G to witness the existential quantifier.

An exact proof term for the current goal is HG.

∎