Aesop proof references unknown private declaration

[JLimperg]

import Aesop

-- works
example {a : Nat} (ha : a = 37) :
    (match matcha : a with
      | 42 => False.elim (by rw [ha] at matcha; sorry)
      | n => n
    ) = 37 := by
  aesop

-- (kernel) unknown constant '_private.AesopTest.Foo.0._example.match_1.eq_2'
example {a : Nat → Nat} (ha : a 0 = 37) :
    (match matcha : a 0 with
      | 42 => False.elim (by rw [ha] at matcha; sorry)
      | n => n
    ) = 37 := by
  aesop