Let X, f and g be given.

Assume Hfg.

Apply set_ext to the current goal.

Apply famunion_Subq to the current goal.

Let x be given.

Assume Hx.

rewrite the current goal using Hfg x Hx (from left to right).

Apply Subq_ref to the current goal.

Apply famunion_Subq to the current goal.

Let x be given.

Assume Hx.

rewrite the current goal using Hfg x Hx (from left to right).

Apply Subq_ref to the current goal.

∎