Let Y, Z, x and u be given.

Assume Hu.

Let p be given.

Assume H1.

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

Let y be given.

Assume Hy: y ∈ Y.

Assume Hu1.

Apply ReplSepE_impred Z (λz ⇒ 0 < y + z) (λz ⇒ (x + y * z) :/: (y + z)) u Hu1 to the current goal.

Let z be given.

Assume Hz: z ∈ Z.

Assume Hyz: 0 < y + z.

Assume Hu2: u = (x + y * z) :/: (y + z).

An exact proof term for the current goal is H1 y Hy z Hz Hyz Hu2.

∎