Simplify the optimizer proof

I think the proof of the optimizer could be simplified by replacing the optimize function that lives in the typed world by an inductive relation. This relation would have a constructor for each optimisation step + constructors for being a congruence.

The main lemmas of the optimizer proof would be:

• forall i : typed instruction, there exists an i' of the same type such that (optimizer_rel i i') and optimize (untype i) = untype i'
• forall i i' such that optimizer_rel i i', (eval i) is equivalent to (eval i')

I think it would be simpler because:

• inductive relations that specify each step of the typed optimizer are already used in the proof
• the exact structure of the optimizer does not need to be followed so closely as in the current proof, the relation can be a superset of what is actually used in the untyped world.

The main benefit of simplifying the proof is that it would become easier to add more optim rules afterward.