github.com/coq/opam-coq-archive
Coq proof of the Gödel-Rosser 1st incompleteness theorem
opam install coq-goedel.8.12.0