Let X be given.

rewrite the current goal using (binunion_com X Empty) (from left to right).

An exact proof term for the current goal is (binunion_idl X).

∎