github.com/coq/opam-coq-archive
An Impredicative Model of Nuprl's Constructive Type Theory
opam install coq-intuitionistic-nuprl.8.6.0