Let Xi and x be given.

Assume Hx: x ∈ coherent_union Xi.

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

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

Use reflexivity.

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

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

An exact proof term for the current goal is Hx.

Apply (UnionE_impred Fam x HxU (∃i : set, i ∈ ω ∧ x ∈ apply_fun Xi i)) to the current goal.

Let G be given.

Assume HxG: x ∈ G.

Assume HG: G ∈ Fam.

Apply (ReplE_impred ω (λj : set ⇒ apply_fun Xi j) G HG) to the current goal.

Let i be given.

Assume HiO: i ∈ ω.

Assume Heq: G = apply_fun Xi i.

We use i to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HiO.

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

An exact proof term for the current goal is HxG.

∎