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