proposition: Lemma Always_Infinite : forall (P:LList A -> Prop) (l:LList A), satisfies l (Always P) -> Infinite l.
proof: Proof. intro P; cofix H. simple destruct l. - inversion 1. - intros a0 l0 H0; split. apply H; auto. inversion H0; auto. Qed.
imports: Arith List RelationClasses