proposition: Lemma diff_comm : forall T eq, forall l1 l2 l3 : list T, diff eq l1 (diff eq l2 l3) = diff eq l2 (diff eq l1 l3).
proof: Proof. induction l1; simpl; sp. rewrite <- diff_remove. rewrite IHl1; auto. Qed.
imports: UsefulTypes bin_rels Omega