Extend the definition of the substitution operation [x::= g] so it applies to ae's with applications and so that the Substitution Lemma will continue to hold. Prove it. (Substitution into an application will now generally have to include renaming lambda-bound identifiers to avoid "false capture.")