Set simplification lemmas appear to cause slowdown

From @PetarMax :
I am not understanding why my lemmas PR is making the Haskell backend CI much slower. I am suspecting it is the set-related lemmas, but they are now minimal and much more concrete:

  // ########################
  // Set Reasoning
  // ########################

    rule S:Set |Set SetItem( X ) => S requires X in S [concrete(X), simplification]

    rule X in S:Set SetItem ( Y ) => true   requires X ==Int Y  [concrete(X, Y), simplification]
    rule X in S:Set SetItem ( Y ) => X in S requires X =/=Int Y [concrete(X, Y), simplification]

and I really would not want to have terms like ((A |Set SetItem (X)) |Set SetItem (Y)) |Set SetItem(X) in my configurations.

We should run an analysis of these simplification lemmas to check what is happening (especially whether and how many times they fail).

Start with the linked lemmas PR and the Haskell backend CI slowdown. Analyze the three Set simplification lemmas, especially whether they fail and how often; done means explaining their contribution to the slowdown and the observed term growth.