proposition: Lemma diff_remove : forall T eq, forall l1 l2 : list T, forall x, diff eq l1 (remove eq x l2) = remove eq x (diff eq l1 l2).
proof: Proof. induction l1; simpl; sp. repeat (rewrite IHl1). rewrite remove_comm; auto. Qed.
imports: UsefulTypes bin_rels Omega