proposition: Lemma OO_is_infiniteII : Inf Nat (fun x y : Nat => Le y x) OO.
proof: Proof. cofix u. apply (inf Nat (fun x y : Nat => Le y x) OO OO). pattern OO at 2 in |- *. rewrite OO_unfold. apply Le_n. apply u. Qed.
imports: Acc_and_Inf