github.com/coq/opam-coq-archive
The confluence of Hardin-Lévy lambda-sigma-lift-calcul
opam install coq-subst.8.10.0