∀ {α : Sort u_1} (ctx : Lean.Data.AC.Context α),
  Std.Commutative ctx.op →
    ∀ (x : ℕ) (xs : List ℕ),
      Lean.Data.AC.evalList α ctx (Lean.Data.AC.sort (x :: xs)) =
        Lean.Data.AC.evalList α ctx (x :: Lean.Data.AC.sort xs)