Let Y, x, X, g and z be given.

Assume Hz.

Let p be given.

Assume H1.

Apply famunionE_impred Y (λy ⇒ {(1 + (x' + - x) * y) * g x'|x' ∈ X}) z Hz to the current goal.

Let y be given.

Assume Hy.

Assume H2: z ∈ {(1 + (x' + - x) * y) * g x'|x' ∈ X}.

Apply ReplE_impred X (λx' ⇒ (1 + (x' + - x) * y) * g x') z H2 to the current goal.

Let x' be given.

Assume Hx': x' ∈ X.

Assume H3: z = (1 + (x' + - x) * y) * g x'.

An exact proof term for the current goal is H1 y Hy x' Hx' H3.

∎