proposition: Lemma disjoint_cons_l : forall T x, forall l1 l2 : list T, disjoint (x :: l1) l2 <=> disjoint l1 l2 # ! LIn x l2.
proof: Proof. intros; sp. trw disjoint_sym. trw disjoint_cons_r. trw disjoint_sym; split; auto. Qed.
imports: UsefulTypes bin_rels Omega