proposition: Lemma last_eq_middle_inv : forall x y l1 l2 l, l & x = l1 & y ++ l2 -> (l = l1 /\ x = y /\ l2 = nil) \/ (exists l2', l2 = l2'&x).
proof: Proof. Proof using. introv E. destruct (last_case l2) as [|(z&t&K)]. { subst. rew_list in *. lets (?&?): last_eq_last_inv E. left*. } { subst. repeat rewrite <- app_assoc in E. lets (?&?): last_eq_last_inv E. subst. right*. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)