Let X and Fam be given.

Assume Hsub: X ⊆ ⋃ Fam.

We will prove covers X Fam.

Let x be given.

Assume HxX: x ∈ X.

We will prove ∃u : set, u ∈ Fam ∧ x ∈ u.

We prove the intermediate claim HxU: x ∈ ⋃ Fam.

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

Apply (UnionE Fam x HxU) to the current goal.

Let u be given.

Assume Hpack: x ∈ u ∧ u ∈ Fam.

We prove the intermediate claim Hxu: x ∈ u.

An exact proof term for the current goal is (andEL (x ∈ u) (u ∈ Fam) Hpack).

We prove the intermediate claim HuFam: u ∈ Fam.

An exact proof term for the current goal is (andER (x ∈ u) (u ∈ Fam) Hpack).

We use u to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HuFam.

An exact proof term for the current goal is Hxu.

∎