proposition: Lemma L3 : forall (w: LList nat), satisfies w (Eventually P) -> exists n : nat, LNth n w = Some 0.
proof: Proof. induction 1. - generalize H; case a; simpl in H. + now exists 0. + contradiction. - case IHEventually; intros p Hp; exists (S p); cbn ; auto. Qed.
imports: chap13