Hi, I was having issues running this in Coq 8.19. The following minor changes fixed the issues for me: * Replacing `plus_0_r` and `plus_0_l` with `Nat.add_0_r` and `Nat.add_0_l` in `DeBruijn.v` . * Replacing `elimtype False` with `exfalso` in `Environments.v` I have made a corresponding pull request: https://github.com/coq-community/dblib/pull/15