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

auto uint_equal

uint_equal: (all x:Nat, y:Nat. (fromNat(lit(x)) = fromNat(lit(y))) = (x = y))

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

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

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