The Coq mailing list

[Christian Urban <curban AT cs.princeton.edu>]

Hi Flavio,

> I am interested on a formalization of the substitution lemma in de  
> Bruijn notation (in Coq). I saw some discussion in coq-club about  
> substitution lemma, but I didn't find nothing in de Bruijn notation  
> anywhere. Does anyone know a formalization of the substitution lemma  
> in de Bruijn notation?

At LFMTP'06, Stefan Berghofer and I wrote about
the substitution lemma in de Bruijn notation in
the context of the lambda-calculus and Nominal
Isabelle.

 http://www4.in.tum.de/~urbanc/Publications/lfmtp-06.ps

There we included all reasoning steps involved to
formalise this lemma. They should be easily portable to
Coq. In fact the material was transmitted to us via
Nipkow and Rasmussen from a formalisation by Huet in
Coq. See references in the paper.

Maybe this is of help,
Christian