proposition: Lemma prefix_closure_singleton: forall ys : list A, (fun xs => prefix xs ys) = prefix_closure (= ys).
proof: Proof. Proof using. intros. extens; intros xs. unfold prefix_closure. split. eauto. intros (?&?&?). subst. eauto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)