coq-schroeder

The Theorem of Schroeder-Bernstein. Fraenkel's proof of Schroeder-Bernstein theorem on decidable sets is formalized in a constructive variant of set theory based on stratified universes (the one defined in the Ensemble library). The informal proof can be found for instance in "Axiomatic Set Theory" from P. Suppes.

opam install coq-schroeder.8.5.0
homepage
https://github.com/coq-contribs/schroeder
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/schroeder/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/schroeder/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-schroeder/coq-schroeder.8.5.0