update proof of exp_to_i3_correct