Current status: new definition of Instr.t, but has to be changed to remove reductions of match ... with eq_refl => ...
Complete reduction of the evaluation