The Coq mailing list

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

It's certainly true that such parameter declarations act as implicit 
binders for the parameter variables, across the whole rest of the 
inductive definition.  The function arrow [->] is a special case of 
[forall], so the _type_ of your inductive type family will involve 
[forall], no matter what you do, as long as there are any parameters.  
By definition, a type family with parameters must have all constructors' 
types end in instances of that type family applied to exactly the 
parameter variables.  So, if you used an explicit [forall] in a 
constructor to bind a different variable to pass as the parameter value 
at the end of some constructor type, that would be an error.  (Though 
you may change the parameter values in the _arguments_ of a constructor, 
just not the _result_ type)

I feel like I'm probably missing the heart of your question, so let me 
know if I haven't answered it.

Patricia Peratto wrote:
> I mean by parameter the name of variable together with
> its type that one puts to the left of the : in  a definition,
> by example A:Type in
> Inductive List (A:Type):Type
> or
> (A:Type) and (x:A) in
> Inductive eq (A:Type)(x:A) : A->Type
...
> Is true that with  parameters and -> I don't need forall?
> or is there a case in which forall is necesary?