The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Are any one of the following two opposite statements provable in Coq  
(with or without the boolean assumption):

1. there exist types A, B, C such that A->(B->C) is not equal to B-> 
(A->C)
2. for all A, B, C one has A->(B->C) = B->(A->C)

If neither one is provable can one prove (outside of coq) that both  
are not provable?

Vladimir.