law u32_to_nat_inj

bend-kit-lemmas@0.1.1.0 · lemmas.bend:265

import Base

265law u32_to_nat_inj:
266  for a: U32
267  for b: U32
268  for h: {U32.to_nat(a) == U32.to_nat(b) : Nat}
269  {a == b : U32}