Add proof for the Var case of subst lemma

Lots of omega cheating, but whatever.