rewrite gmultiset_disj_union typeclass blow up

The following rewrite gmultiset_elements_disj_union blows up typeclass search quite a lot.

Lemma test {A B} `{Countable A} `{Countable B}
      (xs : list (A * B)) (X Y: gmultiset (A * B)) :
  xs ++ elements (X ⊎ Y)  ≡ₚ xs ++ (elements X ++ elements Y).
Proof.
  Set Typeclasses Debug.
  by rewrite gmultiset_elements_disj_union.
Qed.

Debug log is ~85k lines. Using simpler types (like A * B instead of A * list B) the debug log is shorter, and it terminates faster. Just using A is ~2.5k lines.

Removing the xs ++ _ prepend makes the blow up seem linear. So does suffixing the xs instead (_ ++ xs)