proposition: Lemma eventually_to_dist : forall A (P:A->Prop) s, eventually P s -> exists n, first_st_at P s n.
proof: Proof. Proof using. introv H. induction H. exists 0. simple~. destruct (prop_inv (P x)). exists 0. simple~. destruct IHeventually as [n Pn]. exists (S n). simple~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibFun LibEpsilon LibList LibInt LibNat LibProd LibSum LibRelation LibWf LibFix LibStream) ZifyNat