Let U be given.

Assume HU: open_cover X Tx U.

Set pick to be the term (λx : set ⇒ Eps_i (λu : set ⇒ u ∈ U ∧ x ∈ u)).

Set V to be the term {pick x|x ∈ X}.

We use V to witness the existential quantifier.

Apply andI to the current goal.

We will prove V ⊆ U ∧ countable_set V.

Apply andI to the current goal.

Let v be given.

Assume HvV: v ∈ V.

Apply (ReplE_impred X (λx0 : set ⇒ pick x0) v HvV (v ∈ U)) to the current goal.

Let x be given.

Assume HxX: x ∈ X.

Assume HvEq: v = pick x.

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

We prove the intermediate claim Hcov: covers X U.

An exact proof term for the current goal is (open_cover_implies_covers X Tx U HU).

We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ x ∈ u.

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

We prove the intermediate claim Hp: pick x ∈ U ∧ x ∈ pick x.

An exact proof term for the current goal is (Eps_i_ex (λu : set ⇒ u ∈ U ∧ x ∈ u) Hexu).

An exact proof term for the current goal is (andEL (pick x ∈ U) (x ∈ pick x) Hp).

We will prove countable_set V.

An exact proof term for the current goal is (countable_image X HcountX (λx0 : set ⇒ pick x0)).

We will prove covers X V.

Let x be given.

Assume HxX: x ∈ X.

We use (pick x) to witness the existential quantifier.

We will prove pick x ∈ V ∧ x ∈ pick x.

Apply andI to the current goal.

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

We prove the intermediate claim Hcov: covers X U.

An exact proof term for the current goal is (open_cover_implies_covers X Tx U HU).

We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ x ∈ u.

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

We prove the intermediate claim Hp: pick x ∈ U ∧ x ∈ pick x.

An exact proof term for the current goal is (Eps_i_ex (λu : set ⇒ u ∈ U ∧ x ∈ u) Hexu).

An exact proof term for the current goal is (andER (pick x ∈ U) (x ∈ pick x) Hp).