Remove `apply_closure` from semantics

PureLang, ThunkLang, and EnvLang all use a function called `apply_closure` in their semantics. With the changes from #31, this seems unnecessary - `apply_closure` should instead be replaced by straightforward function application. This should simplify various proofs, particularly in ThunkLang where removing lemmas concerning `apply_closure` will likely streamline things.

Care needs to be taken for `Ret`/`Raise` in ThunkLang/EnvLang - these are now call-by-value, i.e. they evaluate the contained argument no matter what. This is achieved by a combination of `with_value`/`apply_closure` currently.

Start with the PureLang, ThunkLang, and EnvLang semantics and the changes from #31. Trace each use of apply_closure and the related with_value handling, paying particular attention to call-by-value Ret and Raise in ThunkLang and EnvLang. Done means direct function application replaces apply_closure and the affected proofs, especially in ThunkLang, no longer need its lemmas.

Written by the indexing model from the issue text.