Is there a limit of sin_rewrite etc. ?

[JonasOberhauser]

Goal forall a b c d e f g h i : relation actid, a ⨾ b ⨾ c ⨾ d ⨾ e ⨾ f ⨾ g ⨾ h ⨾ i ⊆ ∅₂.
Proof.
  intros.
  arewrite (a ⨾ b ⨾ c ⨾ d ⨾ e ⨾ f ⨾ g ⨾ h ⊆ ∅₂).

fails. Am I doing something wrong or did I reach some internal limit of sin_rewrite etc?

[JonasOberhauser]

If it's an internal limit, would it be much effort to switch to this: https://github.com/coq-community/aac-tactics ? This could also work for ∩ etc.