proposition: Lemma disjoint_diff_l : forall A eq, forall l1 l2 l3 : list A, disjoint (diff eq l1 l2) l3 <=> disjoint l2 (diff eq l1 l3).
proof: Proof. induction l1; simpl; sp. trw IHl1. rewrite diff_remove. trw disjoint_remove_l. split; sp. Qed.
imports: UsefulTypes bin_rels Omega