proposition: Lemma map_eq_app_inv : forall f l r1 r2, map f l = r1 ++ r2 -> exists l1 l2, l = l1++l2 /\ r1 = map f l1 /\ r2 = map f l2.
proof: Proof. Proof using. intros f l. induction l as [|x l']; introv E. { rewrite map_nil in E. lets (?&?): nil_eq_app_inv E. subst. exists* (@nil A) (@nil A). } { rewrite map_cons in E. destruct r1 as [|y r1']; rew_list in E. { exists* (@nil A) (x::l'). } { invert E ;=> N1 N2. forwards (l1'&l2&E1&E2&E3): IHl' N2. exists (x::l1') l2. subst*. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)