Let Xi and i be given.

Assume HiO: i ∈ ω.

Let x be given.

Assume Hx: x ∈ apply_fun Xi i.

An exact proof term for the current goal is (coherent_union_contains Xi i x HiO Hx).

∎