proposition: Lemma flat_map_app: forall (A B : Type) (f : A -> list B) (l l' : list A), flat_map f (l ++ l') = flat_map f l ++ flat_map f l'.
proof: Proof. induction l as [| a l Hind]; introv;sp. simpl. rw <- app_assoc. f_equal. sp. Qed.
imports: UsefulTypes bin_rels Omega