proposition: Lemma map_eq_middle_inv : forall f l r1 y r2, map f l = r1 ++ y :: r2 -> exists l1 x l2, l = l1++x::l2 /\ r1 = map f l1 /\ y = f x /\ r2 = map f l2.
proof: Proof. Proof using. introv E. lets (l1&l2'&E1&E2&E3): map_eq_app_inv (rm E). lets (x&l2&E4&E5&E6): map_eq_cons_inv (eq_sym E3). exists l1 x l2. subst*. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)