start work on correctness of translation to IL4

currently annoyed by the possibility of a recursive closure whose
function names are not ALL_DISTINCT: this can matter when switching to
de Bruijn. this commit includes a good_v_i2 predicate, but that is a
annoying to carry around; I think a nicer method might be to make
do_app_i2 stronger and make it do the check.