Let x be given.

We will prove x ∪ {u ''|u ∈ 0} = x.

rewrite the current goal using Repl_Empty (λu ⇒ u '') (from left to right).

We will prove x ∪ 0 = x.

An exact proof term for the current goal is binunion_idr x.

∎