proposition: Fact map_duplicate_inv ll l' y1 m' y2 r' : map f ll = l'++y1::m'++y2::r' -> { l : _ & { x1 : _ & { m : _ & { x2 : _ & { r | l' = map f l /\ y1 = f x1 /\ m' = map f m /\ y2 = f x2 /\ r' = map f r /\ ll = l++x1::m++x2::r } } } } }.
proof: Proof. intros H1. apply map_middle_inv in H1. destruct H1 as (l & x1 & k & H1 & H3 & H4 & H5). apply map_middle_inv in H5. destruct H5 as (m & x2 & r & -> & H6 & H7 & H8). now exists l, x1, m, x2, r. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)