Let Y, x, X, g and h be given.
Assume Hgh.
We will prove (yY{(1 + (x' + - x) * y) * g x'|x'X}) = (yY{(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'.