github.com/coq/opam-coq-archive
A normalization proof a la Tait for simply-typed lambda-calculus
opam install coq-tait.8.10.0