law u32_to_nat_inj

bend-mathlib@0.8.1.0 · u32.bend:517

import Base

517# Distinct U32s have distinct values: to_nat a = to_nat b implies a = b.
518law u32_to_nat_inj:
519  for a: U32
520  for b: U32
521  for e: {U32.to_nat(a) == U32.to_nat(b) : Nat}
522  {a == b : U32}