The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Tie Cheng wrote:
> where "∀ a1:A, ∀ a2:List A" matches "∀ a1:A1, ∀ a2:A2" of the formula 
> "C≡ ∀ p1:P1,…,∀ pr:Pr,∀ a1:A1, … ∀ an:An, (I p1 … pr t1… tq)", so A is 
> A1, List A is A2 here.
>
> On the other hand, in the previous example in the manual, they mention 
> "Assuming ΓI is [I1:A1;…;Ik:Ak]". As we have [List:Set→Set] as ΓI in 
> this exemple, "Set→Set" should match A1. So here comes 
> the contradiction: I do not see how "Set→Set" could be A or List A via 
> A1 or A2.

I don't see any prose in the manual that suggests these two sets of [A] 
variables are meant to be the same.  I think it's just a case of 
choosing the same metavariable in logically unrelated places, so that 
there is no contradiction.