The Coq mailing list

[Tie Cheng <chengtie AT gmail.com>]

OK... I understand better, thank you...

Tie

On Fri, May 6, 2011 at 4:28 PM, Adam Chlipala <adam AT chlipala.net> wrote:

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.