github.com/coq/opam-coq-archive
Nfix: a Coq extension for fixpoints on nested inductives
opam install coq-nfix.8.8.0