Added a lemma about compiling application expressions

modLang and conLang proofs both had a separate lemma abut compiling
applications, so I've added an analogous one for exhLang.