Let X, F and G be given.

Assume H1: ∀x ∈ X, F x = G x.

Apply set_ext to the current goal.

An exact proof term for the current goal is ReplEq_ext_sub X F G H1.

Apply ReplEq_ext_sub X G F to the current goal.

Let x be given.

Assume Hx.

Use symmetry.

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

∎