github.com/coq/opam-coq-archive
A direct constructive proof of Higman's Lemma
opam install coq-higman-cf.8.10.0