Let X, f and g be given.

Assume Hfg.

Let y be given.

Assume Hy.

Apply famunionE_impred X f y Hy to the current goal.

Let x be given.

Assume Hx.

Assume H1: y ∈ f x.

Apply famunionI X g x y Hx to the current goal.

We will prove y ∈ g x.

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

∎