The normal form is not robust. Substitution breaks an invariant of the normal form.

[FardaleM]

Currently, the normal form is not stable by substitution. Tuples are represented as sorted arrays, this property is not preserved by substitution. There are 3 possible ways to fix it:

1. Change the normal form and remove the constraint on the array to be sorted. This solution has an impact on the equivalence test, which currently relies on this property.
2. Do the sorting after the substitution. Could have an impact on speed
3. Use another representation that preserves the equivalence modulo AC.

Also, one need to check that replacing a variable in the head position by an arrow is currently correctly handle.