∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (s₁ s₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx (s₁.union s₂) =
    ctx.op (Lean.Grind.AC.Seq.denote ctx s₁) (Lean.Grind.AC.Seq.denote ctx s₂)