work on IL4 translation correctness

bite the bullet and use the good_v_i2 predicate and prove evaluate_i3
preserves it...

attempting to prove things about pat_to_i4 and it's surprisingly subtle
and long, but basically going through.

finished skeleton of exp_to_i4_correct, with cheats mostly for pattern
matching.