proposition: Lemma fold_left_flat_map : forall bs l, fold_left f bs l = flat_map g (rev bs) ++ l.
proof: Proof. induction bs; simpl; intro. refl. rewrite IHbs, hyp, flat_map_app, app_ass. simpl. rewrite <- app_nil_end. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)