Failing to unify with sets

Stream: new members

[James Reynolds]

I'm working on formalising some type systems in Lean. In trying to apply typing rules I frequently have to do several tedious set-related rewrites before Lean can unify successfully. I've included the most minimal example of this kind of difficulty I can come up with. Is there a better way of allowing the rule to unify than rewriting manually? Ideally I'd just like to let aesop do this, but even after the rewrite it still fails for me. Am I missing something there?

import Mathlib

@[aesop unsafe constructors]
inductive Cons : (Set Nat) → Prop
  | A : (Γ : Set Nat) → (A : Nat) → Cons (Γ ∪ {A})

example : Cons {5} := by
  --apply Cons.A ∅ 5              -- This doesn't work
  --exact?                        -- This doesn't work
  --aesop                         -- This doesn't work

  -- With a preceding rewrite:
  rw [←Set.empty_union {5}]
  --apply Cons.A                  -- This works
  --exact?                        -- This works
  --aesop                         -- This doesn't work