He supposes it's good that people are finding so many detailed ways to be wrong, exhibiting them early and getting them out of the way.
"We haven't said anything about adding - outside the system, up at our level - rules for adding in parentheses that weren't in the written form. So that could mean either -"
\k. ((k=0 /\ k + k = k) \/ ~(k=0)) /\ ~(k + k = k)
\k, (k=0 /\ k + k = k) \/ (~(k=0) /\ ~(k + k = k))