The Coq mailing list

["Flavio L. C. de Moura" <flaviomoura AT unb.br>]

Hi there,

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?


Thanks in advance!

Flávio.