The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 10/03/2013 01:40 PM, Fabien Renaud wrote:
> I know that in my example the property is not true in general.
>
> I would like to know if there is a way to restrict the statement on
> NList_ which have been created by NList (for which the statement is true).
You should probably give a more illustrative example. Here, any sensible 
restriction is the same as the property you wish to prove.

The best result you well get in this case is:

  Goal forall A (l : list A) n, NList_ n l -> n <= length l.
  Proof. induction 1; simpl; auto with arith. Qed.