proposition: Lemma flat_map_app : forall l m, flat_map f (l ++ m) = flat_map f l ++ flat_map f m.
proof: Proof. induction l; simpl; intros. refl. rewrite IHl, app_ass. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)