Add proof of subst lemma

Lots of omega cheating in the var case, but whatever.