The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

> I suspect that your question is related to continuity.
> 
> Streams over A are (extensionally) isomorphic to (Nat -> Nat). Any  
> function of type (Nat -> Nat) -> Nat can only access a finite segment  
> of its input. This is known as "local continuity" or formally
> 
> forall f:Nat -> Nat, exists n:Nat, forall g,h : Nat, -> Nat,(forall  
> i:Nat,i < n -> g i = h i) -> f g = f h

I naively thought that a variation on this seems to characterize 
my "inductively_defined" predicate, i.e. 

Definition inductively_defined P := 
 exists n:Nat, forall g,h : Nat -> Nat, 
 (forall i:Nat,i < n -> g i = h i) -> P g <-> P h

But this would exclude "eventually", given by Eduardo, since I cannot fix n.
Could you suggest any fix?

Best,
Keiko