proposition: Lemma disjoint_flat_map_r : forall A B, forall f : A -> list B, forall l1 : list A, forall l2 : list B, disjoint l2 (flat_map f l1) <=> (forall x, LIn x l1 -> disjoint l2 (f x)).
proof: Proof. sp. rw disjoint_sym. rw disjoint_flat_map_l; split; sp; rw disjoint_sym; sp. Qed.
imports: UsefulTypes bin_rels Omega