Add assert_total function

This marks its argument as total, meaning that smaller subexpressions
can now be asserted to be total, rather than entire functions. A
combination of assert_smaller and assert_total should be used to help
the totality checker, rather than %assert_total to mark an entire
function as total.

The %assert_total option will be removed later.
Remove %assert_total from Nat and Strings