Adding certain rules causes kernel error in later theorem

[hgoldstein95]

I'm not 100% sure this is an Aesop problem, it could be a core Lean issue, but I can't get the issue to happen without Aesop so I'm starting here.

Here's an example of a couple of very simple theorems:

import Aesop

theorem foo
    {T : Prop → Prop}
    (h : ∀ v, T (v = 2)) :
    ∀ v, T (2 = v) := by
  aesop? (add unsafe (by simp_all [eq_comm]))

theorem bar (h : Q ∧ P) : P ∧ Q := by
  simp_all [and_comm]

Aesop easily solves foo, suggesting the proof intro v; (simp_all [eq_comm]) as expected, but then bar fails with the message "(kernel) constant has already been declared 'Module._auxLemma.1'".

If I replace the call to aesop with the suggested proof, everything compiles correctly.

Any idea what's going on?