proposition: Lemma disjoint_remove_l : forall A eq x, forall l1 l2 : list A, disjoint (remove eq x l1) l2 <=> disjoint l1 (remove eq x l2).
proof: Proof. induction l1 as [| ? l IHl1] ; simpl; sp; split; sp. trw disjoint_cons_l; sp. trw_rev IHl1. destruct (eq x a); subst; auto. alltrewrite disjoint_cons_l; sp. destruct (eq x a); subst; auto. alltrewrite in_remove; sp. alltrewrite disjoint_cons_l; sp. alltrewrite in_remove; sp. alltrewrite disjoint_cons_l; sp. destruct (eq x a); subst; auto. trw IHl1; auto. alltrewrite disjoint_cons_l; sp. trw IHl1; auto. allrw in_remove; sp. Qed.
imports: UsefulTypes bin_rels Omega