proposition: Fact flat_map_app_inv l r1 y r2 : flat_map f l = r1++y::r2 -> exists l1 m1 x m2 l2, l = l1++x::l2 /\ f x = m1++y::m2 /\ r1 = flat_map f l1++m1 /\ r2 = m2++flat_map f l2.
proof: Proof. revert r1 y r2. induction l as [ | x l IHl ]; intros r1 y r2 H. + destruct r1; discriminate. + simpl in H. apply list_app_cons_eq_inv in H. destruct H as [ (m & Hm1 & Hm2) | (m & Hm1 & Hm2) ]. - apply IHl in Hm2. destruct Hm2 as (l1 & m1 & x' & m2 & l2 & G1 & G2 & G3 & G4); subst. exists (x::l1), m1, x', m2, l2; simpl; repeat (split; auto). rewrite <- app_assoc; auto. - exists nil, r1, x, m, l; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)