The Coq mailing list

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

I might be misunderstanding something, but 

> It would be an inductive definition without any reference to infinite
> types or terms. 

how I can define a predicate on predicates of type LList -> Prop 
which states that a given predicate is defined without any reference to 
infinite objects?

Kind regards,
Keiko