github.com/coq/opam-coq-archive
A Coq Library of Undecidability Proofs
opam install coq-library-undecidability.1.0.0+8.12