implies a strongly classical world. Especially it conflicts with
impredicativity of Set, knowing that true<>false in Set.
- [1] Laurent Chicli, Loïc Pottier, Carlos Simpson, Mathematical
+ [1] Laurent Chicli, Lo\239\c Pottier, Carlos Simpson, Mathematical
Quotients and Quotient Types in Coq, Proceedings of TYPES 2002,
Lecture Notes in Computer Science 2646, Springer Verlag.
*)