github.com/coq/opam-coq-archive
Explicit Convertibility Proofs in Pure Type Systems
opam install coq-ptsf.8.10.0