Adjust Lemma 3 proof to new definition of configuration typing

[aigarashi]

This is not that hard of a change; since we only really invert in the Deref case, we just need to appeal to Lemma 4/5.