proposition: Theorem from_Infinite_V0 : forall n:nat, Infinite (from n).
proof: Proof. Proof (cofix H : forall n:nat, Infinite (from n) := F_from H). Lemma from_Infinite : forall n:nat, Infinite (from n). Proof. cofix H. - intro n; rewrite (from_unfold n); now split. Qed.
imports: Arith List RelationClasses