slowly working through making exp_to_i4_correct use a relation

updated the relation on expressions so it knows the number of bound
variables they expect... it is slowly becoming more and more like
full-blown syneq. might want to make sure the hard cases of
exp_to_i4_correct will go through with the current version before
proving the rest...