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