Define two function pred and sub for predecessor and subtraction, respectively. As we are modeling the natural numbers, the predecessor of zero is zero, and subtraction is truncated at zero. For example, sub(from_int(3), from_int(5)) should return from_int(0), not from_int(-2).

Updated: