import Base

import Nat

import UIntDefs

from_zero: fromNat(ℕ0) = 0

from_one: fromNat(ℕ1) = 1

toNat_dub: (all x:UInt. toNat(dub(x)) = ℕ2 * toNat(x))

toNat_inc: (all x:UInt. toNat(inc(x)) = suc(toNat(x)))

toNat_pred: (all x:UInt. toNat(pred(x)) = pred(toNat(x)))

to_fromNat: (all x:Nat. toNat(fromNat(x)) = x)

toNat_injective: (all x:UInt, y:UInt. (if toNat(x) = toNat(y) then x = y))

from_toNat: (all b:UInt. fromNat(toNat(b)) = b)

fromNat_injective: (all x:Nat, y:Nat. (if fromNat(x) = fromNat(y) then x = y))