This page is dedicated to the formal proof in Coq of the linear explicit substitutions and strong normalization.
The full code is downloadable here (Coq 8.5pl2)
You may also want to browse the library by the index or by clicking the dependence graph:
