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