proposition: Lemma diff_dup : forall T eq, forall l1 l2 l3 : list T, forall x, LIn x (l1 ++ l2) -> diff eq (l1 ++ l2) l3 = diff eq (l1 ++ x :: l2) l3.
proof: Proof. induction l1; simpl; sp; subst. rewrite diff_remove. apply remove_dup; auto. rewrite diff_move; simpl. rewrite <- remove_repeat; auto. Qed.
imports: UsefulTypes bin_rels Omega