proposition: Lemma prefix_closed_nil: forall (P : list A -> Prop) xs, prefix_closed P -> P xs -> P nil.
proof: Proof. Proof using. eauto with prefix. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)