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