proposition: Lemma prefix_last: forall x xs ys, prefix (xs & x) ys -> prefix xs ys.
proof: Proof. Proof using. introv [ zs ? ]. exists (x :: zs). rew_list in *. eauto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)