proposition: Lemma prefix_cons_cons: forall x xs1 xs2, prefix xs1 xs2 -> prefix (x :: xs1) (x :: xs2).
proof: Proof. Proof using. introv (ys&?). subst. exists ys. rew_list. eauto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)