Indexing failure involving `Quotient.sound`

[JLimperg]

MWE:

import Aesop

instance Multiset'.Setoid (α : Type) [BEq α] : Setoid (List α) where
  r as bs := ∀x, List.count x as = List.count x bs
  iseqv := by refine' {..} <;> aesop

def Multiset' (α : Type) [BEq α] : Type := Quotient (Multiset'.Setoid α)

theorem Multiset'.union.extracted_3 {α : Type} [inst : BEq α] (a1 b1 a2 b2 : List α) (h1 : a1 ≈ a2) (h2 : b1 ≈ b2):
  (Quotient.mk (Multiset'.Setoid α) (a1 ++ b1)) = (Quotient.mk' (a2 ++ b2)) := by
  -- apply Quotient.sound -- succeeds
  aesop (add safe apply Quotient.sound) -- no progress