Let Y, Z, x and y be given.

Assume Hy.

Let z be given.

Assume Hz.

Assume H1.

We will prove (x + y * z) :/: (y + z) ∈ ⋃_{y ∈ Y}{(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}.

Apply famunionI Y (λy ⇒ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}) y ((x + y * z) :/: (y + z)) Hy to the current goal.

We will prove (x + y * z) :/: (y + z) ∈ {(x + y * z) :/: (y + z)|z ∈ Z, 0 < y + z}.

An exact proof term for the current goal is ReplSepI Z (λz ⇒ 0 < y + z) (λz ⇒ (x + y * z) :/: (y + z)) z Hz H1.

∎