github.com/coq/opam-coq-archive
Reflexive first-order proof interpreter
opam install coq-reflexive-first-order.8.10.0