More simplifications

[andreistefanescu]

Remove the arrayIte simplification because it actually increases expression size, and combined with the muxing from the memory model can create very large expressions.

[andreistefanescu]

The simplifications are simply the result of me trying different things until the latest aws-lc proof works. There isn't any underlying reason to it. I agree, we should audit and document the existing simplification, and maybe have a more principled/exhaustive way of adding simplifications.