Let U and V be given.

rewrite the current goal using (binunion_eq_Union_UPair U V) (from left to right).

Use reflexivity.

∎