Continue termination proof; some renaming.
Clean up, and one new lemma. (Can you spot it? :)