YES
(VAR vg vh vy ta)
(RULES
c_union(c_insert(vg,vh,vy),ta,vy) -> c_insert(vg,c_union(vh,ta,vy),vy)
c_union(c_Message_Oparts(vg),c_Message_Oparts(vh),tc_Message_Omsg()) -> c_Message_Oparts(c_union(vg,vh,tc_Message_Omsg()))
c_union(c_emptyset(),vg,vh) -> vg
)