The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Georgi Guninski wrote:
> On Sat, Jun 25, 2011 at 09:34:05AM -0400, Adam Chlipala wrote:
>    
> > Neither proof is showing an inconsistency in Coq. Rather, you've
> > shown that [uat_maximal_card] is an inconsistent axiom even by
> > itself, and [uat_not_maximal_card] is inconsistent with
> > [eq_rect_eq].
> >      
> If you examine the coq output, you will find out in both cases:
> ~uat_maximal_card = uat_not_maximal_card
>
> Any ideas on simplifying your statement?
>    

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!