Correct and clean up Redex model a bit.

Using smaller numbers in the tests for LVish-nat so that Redex
doesn't explode.