Let x and y be given.

Assume Hx.

Let u be given.

Assume Hu.

Let v be given.

Assume Huv.

Let w be given.

Assume Hw: w ∈ u.

We prove the intermediate claim L1: w ∈ v ''.

rewrite the current goal using Huv (from right to left).

We will prove w ∈ u ∪ {extension_tag}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hw.

Apply binunionE v {extension_tag} w L1 to the current goal.

Assume H1: w ∈ v.

An exact proof term for the current goal is H1.

Assume H1: w ∈ {extension_tag}.

We will prove False.

We prove the intermediate claim L2: w = extension_tag.

An exact proof term for the current goal is SingE extension_tag w H1.

Apply extension_tag_fresh x Hx u Hu to the current goal.

We will prove extension_tag ∈ u.

rewrite the current goal using L2 (from right to left).

An exact proof term for the current goal is Hw.

∎