Editorial: Add a "safe integer" numerical kind

This patch makes three numeric kinds: safe integers, Numbers and
mathematical values. It also makes the subscript for operations always
implicit--if at least one operand is a Number or mathematical value,
then it is an operation outputting that kind, otherwise it's an operation
on safe integers which implicitly contains an assertion that the output
is a safe integer. This phrasing has significantly fewer subscripts
while (implicitly) including more assertions that semantics aren't
changing.

Overall, I'm not sure if this is the best way to go. Because operations
don't have subscripts, random constants in the expression are enlisted
to have subscripts to force the output into a certain kind. Overall, it
seems like it takes more close reading to figure out what's going on.
I'm wondering if it would be better to require subscripts on all
non-"safe integer" operations. This would require, though, that we use
some different notation for exponentiation, as there's currently no
place to put the subscript.