proposition: Lemma infseq_from_function: forall a, infseq_with_function a -> infseq a.
proof: Proof. intros a0 (f & F0 & Fn). exists (fun a => exists i, f i = a); split. - exists 0; auto. - intros a1 (i1 & F1). subst a1. exists (f (1 + i1)); split; auto. exists (1 + i1); auto. Qed.