proposition: Lemma map_app : forall f l1 l2, map f (l1 ++ l2) = map f l1 ++ map f l2.
proof: Proof. Proof using. intros. unfold map. assert (forall accu, fold_right (fun x acc => f x :: acc) accu (l1 ++ l2) = fold_right (fun x acc => f x :: acc) nil l1 ++ fold_right (fun x acc => f x :: acc) nil l2 ++ accu). { induction l1; intros; simpl. { rew_list. gen accu. induction l2; intros. { auto. } { rew_listx. rewrite~ IHl2. } } { rew_listx. fequals. } } specializes H (@nil B). rew_list~ in H. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)