proposition: Lemma prefix_closure_is_prefix_closed: forall P, prefix_closed (prefix_closure P).
proof: Proof. Proof using. unfold prefix_closed, prefix_closure. introv (zs&?&?). eauto using prefix_transitive. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)