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

Assume Hgh.

We will prove (⋃_{y ∈ Y}{(1 + (x' + - x) * y) * g x'|x' ∈ X}) = (⋃_{y ∈ Y}{(1 + (x' + - x) * y) * h x'|x' ∈ X}).

Apply famunion_ext to the current goal.

Let y be given.

Assume Hy.

Apply ReplEq_ext X (λx' ⇒ (1 + (x' + - x) * y) * g x') (λx' ⇒ (1 + (x' + - x) * y) * h x') to the current goal.

Let x' be given.

Assume Hx'.

We will prove (1 + (x' + - x) * y) * g x' = (1 + (x' + - x) * y) * h x'.

Use f_equal.

An exact proof term for the current goal is Hgh x' Hx'.

∎