proposition: Lemma prefix_closure_eq: forall P, prefix_closure P = prefix_closure_alt P.
proof: Proof. Proof using. intros. extens; intros xs; split; unfold prefix_closure, prefix_closure_alt, prefix. { introv (ys&(zs&?)&?). subst. eauto. } { introv (ys&?). eauto. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)