proposition: Lemma eqsetCommute3 : forall {T : Type} (la lb lc : list T), eqset (la ++ lb ++ lc) (lb ++ la ++ lc).
proof: Proof. intros. rw app_assoc. remember ((la ++ lb) ++ lc) as ll. rw app_assoc. subst. apply eqset_app_if; cpx. apply eqsetCommute. Qed.
imports: UsefulTypes bin_rels Omega