proposition: Lemma prove_prefix_snoc: forall x xs ys zs, xs ++ x :: ys = zs -> prefix (xs & x) zs.
proof: Proof. Proof using. intros. exists ys. rew_list. eauto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)