proposition: Lemma map_eq_app : forall l l1 l2, map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ map l1' = l1 /\ map l2' = l2.
proof: Proof. intro l; induction l as [|a l IHl]; simpl; intros l1 l2 Heq. - symmetry in Heq; apply app_eq_nil in Heq; destruct Heq; subst. exists nil, nil; repeat split. - destruct l1; simpl in Heq; inversion Heq as [[Heq2 Htl]]. + exists nil, (a :: l); repeat split. + destruct (IHl _ _ Htl) as (l1' & l2' & ? & ? & ?); subst. exists (a :: l1'), l2'; repeat split. Qed.
imports: PeanoNat