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