prove main lemma about row_to_i4

namely, that it produces a function on expressions that acts like a
binder of the pattern variables (but possibly more temporary variables
too) in a successful match.

not quite enough to finish exp_to_i4_correct: probably need a lemma
about exp_to_i4 that says something about translating under an
environment with extra temporary names in scope.