Let Xi, i and x be given.

Assume HiO: i ∈ ω.

Assume Hx: x ∈ apply_fun Xi i.

Set Fam to be the term {apply_fun Xi j|j ∈ ω}.

We prove the intermediate claim HXdef: coherent_union Xi = ⋃ Fam.

Use reflexivity.

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

We prove the intermediate claim HXi_i_in: apply_fun Xi i ∈ Fam.

An exact proof term for the current goal is (ReplI ω (λj : set ⇒ apply_fun Xi j) i HiO).

An exact proof term for the current goal is (UnionI Fam x (apply_fun Xi i) Hx HXi_i_in).

∎