add_invariant is called on unsimplified term

In prove.py, KEVM.add_invariant is called. This function takes the contents of the callData cell and adds a predicate asserting something about the length of the callData. Because the term it is called on is unsimplified, it contains function symbols that when evaluated, add new constraints to the path condition. The necessity of supporting the equations needed in the Maude backend to propagate these constraints correctly causes the time spent loading KEVM in the Maude backend to increase from 2 seconds to 15 seconds. Ideally, we would simplify the term we create, then add the invariant using the simplified term. This is not hugely urgent, but it causes quite significantly quality of life improvement for developers working on improving the Maude backend's support for kontrol, so I'd like to know what might be able to be done.

Start in prove.py at the call to KEVM.add_invariant and trace how the callData cell term is constructed and simplified. Check the Maude backend behavior when the invariant is added from the unsimplified versus simplified term, including the resulting path constraints and KEVM loading time. Done means the invariant uses the simplified term without requiring the extra equations that cause the reported slowdown.