The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Patricia Peratto wrote:
> Inductive W (A1:Set)(A2:A1->Set):Type:=
> | sup (b:A1)
>         (u:(x:A2 b)W A1 A2)
>                 : W A1 A2.
> I get the error message:
> Error: The reference x was not found in the current
> environment.

This is a gentle suggestion to find a better book or other source for 
learning Coq, or read more carefully through the one you're using.  I 
don't know why you'd think that the "type" you've given to [u] is valid 
Coq syntax.  (It reminds me of the syntax used by Coq versions from 
about 10 years ago.)