```lean import Aesop example (n a : Nat) : a + n = n + a := by aesop? (add apply safe [((Nat.add_comm n a).symm)]) ``` If the parentheses around the rule are removed, we currently get a parsing failure.