The Coq mailing list

[Taral <taralx AT gmail.com>]

On Tue, Jan 20, 2009 at 2:44 AM, Keiko Nakata
<keiko AT kurims.kyoto-u.ac.jp>
 wrote:
> forall P, inductively_defined P ->
> forall s, P s ->
> exists s', "s' is a finite prefix of s such that P s' holds"

This *is* your definition.

In other words:

Definition take (A : Type) (n : nat) (s : LList A) := match n, l with
| 0, _ => LNil | S n', LCons a l' => LCons a (take n' l') end.

Definition inductively_defined (A B : Type) (P : LList A -> B) :=
    forall s, P s -> exists n, forall n', n <= n' -> P (take n' s).

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown