The Coq mailing list

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

Hello.

At the risk of exposing my ignorance... 

Is it correct that:

Suppose P is a predicate on possibly infinite lists, e.g. LList in CoqArt, 
and (P x) holds for some x.
If the definition of P only "involves" induction, 
then there is a finite prefix x' of x such that (P x') holds.

Assuming it correct, what would "involves" precisely mean?
And how I might be able to state it in Coq?

With best regards,
Keiko