The modifier associative commutative can be slow with large terms

[NotBad4U]

Hi everyone,

I am trying to use the modifier associative commutative to run reflective proof similar to lia and lia from Coq. I would like to use the associative commutative for the normalization of my term.

Here is a gist that contains my experimentation: https://gist.github.com/NotBad4U/bb86fb2c18f9e98b5a82a9c5c6f0d9b1

[NotBad4U]

Maybe @fblanqui and @barras, you can add more details about this issue?