Builtin rules loop on simple goal with negation

[JLimperg]

import Aesop
theorem P Q : ¬ P → ¬ Q → False := by
  aesop

The loop happens because applyHyps transforms not P, not Q |- False into not P, not Q |- P and simp transforms this back into not P, not Q |- False.