proposition: Lemma flat_map_app : forall A B (f : A -> list B) (l1 l2 : list A), flat_map f (l1 ++ l2) = (flat_map f l1) ++ (flat_map f l2).
proof: Proof. intros A B f; fix flat_map_app 1. intros l1; case l1; clear l1. intros l2; apply eq_refl. intros a1 l1 l2; simpl; rewrite (flat_map_app l1 l2); rewrite ass_app; apply eq_refl. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)