The Coq mailing list

[Georgi Guninski <guninski AT guninski.com>]

On Sat, Jun 25, 2011 at 09:34:05AM -0400, Adam Chlipala wrote:
> Georgi Guninski wrote:
> >if you read the message you would realize i was asking about
> >*modifications* of his code. here are two files - one takes T as axiom,
> >the other takes ~T as axiom and in both cases False is proven (one of
> >the proofs should be real unless i miss something)
> 
> 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?

Note I probably need excluded middle.

Note that you can try to prove axioms by removing the comments...