proposition: Lemma disjoint_iff_diff : forall T eq, forall l1 l2 : list T, disjoint l2 l1 <=> diff eq l1 l2 = l2.
proof: Proof. induction l1; simpl; sp. trw disjoint_cons_r. trw IHl1. sp_iff Case; intros; exrepd. - Case "->". rewrite remove_trivial; auto. - Case "<-". assert (!LIn a l2) by (intro i; rw <- H in i; allrw in_diff; sp; allrw in_remove; sp). rewrite remove_trivial in H; auto. Qed.
imports: UsefulTypes bin_rels Omega