proposition: Fact map_middle_inv ll m y n : map f ll = m++y::n -> { l : _ & { x : _ & { r | ll = l++x::r /\ map f l = m /\ f x = y /\ map f r = n } } }.
proof: Proof. intros H. destruct map_app_inv with (1 := H) as (l & r & H1 & H2 & H3). symmetry in H3. destruct map_cons_inv with (1 := H3) as (x & r' & H4 & H5 & H6); subst. exists l, x, r'; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)