proposition: Lemma use_prefix_snoc: forall x xs ys zs, prefix (xs & x) ys -> ys = xs ++ zs -> exists zs', zs = x :: zs'.
proof: Proof. Proof using. introv h ?. subst. forwards: eliminate_common_prefix h. eauto using use_prefix_cons. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)