The Coq mailing list

[andré hirschowitz <ah AT unice.fr>]

.

In my experience, the need for a theorem like this more commonly indicates that some part of the development should be refactored, rather than the need to delve into some new axioms or whatnot.  Could you share more of the context?

Ok! Nevertheless, doesn't it help that  the proposed statement is obviously not true in the groupoid of sets  with bijections as equalities?

ah