lngen Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott Original code by Brian Aydemir