The Coq mailing list

[Mathieu Boespflug <mboes AT tweag.net>]

On Sat, Jun 25, 2011 at 11:52:40AM -0400, Adam Chlipala wrote:
> Georgi Guninski wrote:
> >On Sat, Jun 25, 2011 at 10:51:23AM -0400, Adam Chlipala wrote:
> >>I'm not sure what you're asking, but here's a restatement:
> >>[uat_maximal_card] in full generality is fundamentally incompatible
> >>with Coq.  [uat_not_maximal_card] in full generality is incompatible
> >>with another popular axiom.  Thus, you probably don't want to rely
> >>on either as an axiom!
> >let me point no further than
> >
> >https://sympa-roc.inria.fr/wws/arc/coq-club/2011-06/msg00099.html
> >
> >For your convenience, I am including the proof of [uat_maximal_card] (well 
> >and its negation) here - you can diff(1) against my previous testcases:
> 
> Your proofs prove different facts.  Not all occurrences of the same
> source text represent the same formulas in Coq; every occurrence of
> [Type] has a hidden universe variable, and those variables end up
> with different constraints between the versions.

Perhaps the 

Set Printing Universes.

command should help clear up the confusion. Also,

Print Universes.

to see the current global set of constraints on all universe variables
currently in use by Coq. New constraints to existing variables can
arise as new definitions, theorems, etc are made.

-- Mathieu