finish most of exp_to_Cexp_correct

last cheat requires a lemma about app_to_il in the case when the list of
arguments raises an error.