proposition: Lemma app_map_inv : forall {A B} seq l1 l2 (f: A -> B), l1 ++ l2 = map f seq -> exists l1' l2', seq = l1' ++ l2' /\ l1 = map f l1' /\ l2 = map f l2'.
proof: Proof. induction seq; simpl; intros. exists (@nil A); exists (@nil A); simpl. apply app_eq_nil in H; intuition. destruct l1. rewrite app_nil_l in H. exists (@nil A); exists (a :: seq); simpl; intuition. rewrite <- app_comm_cons in H. inversion H. specialize (IHseq _ _ _ H2). destruct IHseq as [l1' [l2' (seq_eq_app & l1l1' & l2l2') ] ]. exists (a :: l1'); exists (l2'); subst; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts