Looping application of rules (Common case with negation)

[xgenereux]

See here for example:

import Aesop

example (P : Prop) (hP : ¬ P) : False := by
  set_option trace.aesop true in
  aesop

Here it is not a big problem, but in a bigger context, we get a timeout before we reach the 30 application limit.