The Coq mailing list

[Fabien Renaud <Fabien.Renaud AT inria.fr>]

Hello,

The subject of my question is not very clear but my problem yes:

For the illustration, suppose I have this (weird) inductive:

Inductive NList_ {A : Type} : nat -> list A -> Type :=
| Base l: NList_ 0 l
| Cons n l a: NList_ n l -> NList_ (S n) (a::l).

Now I want to start building NList_ such that the first argument is always the length of the list:

Definition NList {A : Type} (l : list A) := NList_ (length l) l.

Is there a way to state properties about NList_ created by NList like

forall l n, NList_ n l -> length l = n?

Thanks,

Fabien