Let x and y be given.

Assume Hx: F x.

Assume H1: y '' ∈ x.

Apply extension_tag_fresh x Hx (y '') H1 to the current goal.

We will prove extension_tag ∈ y ''.

We will prove extension_tag ∈ y ∪ {extension_tag}.

Apply binunionI2 to the current goal.

Apply SingI to the current goal.

∎