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.