Progress on the IL2 verification.

Showed that the closures w/o cenv behave the same as the ones with, at
the expression level. The declaration level is still to do.