Altenkirch wrote (in the unpublished draft α-conversion is easy):

I leave it to the reader to show that (some natural translation function) preserves substitution, i.e. it maps substitutions on named terms as given here to substitution on de Bruijn terms.

I'm trying to show it but I can't (and I doubt that his method is suitable). Does anyone have complete proof?