Let X and Fam be given.

Assume Hcov: covers X Fam.

We will prove X ⊆ ⋃ Fam.

Let x be given.

Assume HxX: x ∈ X.

We will prove x ∈ ⋃ Fam.

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

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

Apply (exandE_i (λu : set ⇒ u ∈ Fam) (λu : set ⇒ x ∈ u) Hexu (x ∈ ⋃ Fam)) to the current goal.

Let u be given.

Assume HuFam: u ∈ Fam.

Assume Hxu: x ∈ u.

An exact proof term for the current goal is (UnionI Fam x u Hxu HuFam).

∎