The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Tie Cheng wrote:
> I do not see how to fill in the "???" part here:
>
> The first case, r = 1 and n = 0:
>
> C (for [cons]) ≡ (∀ A:Set, A → List A → List A) ≡ ∀ A:Set, (List A ???)

I think I see the issue.  Remember that, in Coq, the syntax [A -> B] is 
sugar for [forall x : A, B], where [x] does not appear free in [B].  The 
extra arguments that the constructor takes can be considered as 
[forall]-bound.

In other words, your template above with [???] is, in fact, not a 
complete description of the possibilities.  My earlier advice was bad, 
as n should actually be 2 for [cons].  Sorry!