proposition: Lemma from_Infinite_buggy : forall n:nat, Infinite (from n).
proof: Proof. cofix H. auto with llists. Abort. Lemma omega_repeat_infinite (A:Type): forall a:A, Infinite (omega_repeat a). Proof. intros a; cofix H. rewrite (omega_repeat_unfold a); auto with llists. Qed.
imports: Arith List RelationClasses