fact: Definition prefix_closed (P : list A -> Prop) := forall xs ys, P ys -> prefix xs ys -> P xs.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)