proposition: Lemma prefix_nil_inverse: forall xs, prefix xs nil -> xs = nil.
proof: Proof. Proof using. introv (ys&?). forwards: app_eq_nil_inv. eauto. unpack. eauto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)