proposition: Fact map_app_inv ll m n : map f ll = m++n -> { l : _ & { r | ll = l++r /\ m = map f l /\ n = map f r } }.
proof: Proof. revert m n; induction ll as [ | x ll IH ]; intros m n H. * destruct m; destruct n; try discriminate; exists nil, nil; auto. * destruct m as [ | y m ]; simpl in H. + exists nil, (x::ll); auto. + inversion H; subst y. destruct IH with (1 := H2) as (l & r & H3 & H4 & H5); subst. exists (x::l), r; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)