More cleaning up
Shifting and substitution
Starting the substitution lemma for DeBruijn terms