The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Is there a way to define in Coq the type which can be informally described as 
follows:

1. Given parameters A : Type , a : A .

2. I want to define the type of (infinite) sequences f_0 ,..., f_n, .... where

2a. f_0 : A -> A .

2b. f_{S n} : {| x : A ; f_n x = a |} -> A .

Is there a way to define the type of such sequences ?

Thanks!
Vladimir.