Note 1: For the moment, we provide instances only for numbers that
fit in a Word.  The reason is a quite mundane:  to generate evidence
for arbitrary integers we need to generate integer literals.
In the core syntax this is a monadic operation but the function that
generates the core for evidence is pure.  It would not be hard to monadify
it but requires changes to a bunch of other functions so I thought it
is better left for a separate change.

Note 2: The evidence that we generate for a NatI is just a word.
Technically, we should be generate a word with two coercions: one to
turn it into a NatS and another to turn that into a NatI.  Operationally,
these do not do anything, but it would be better to fix this.  I didn't
do it yet because I need to look up how to make these coercions.