law to_nat_inj

lawful-words@0.1.0.0 · proof_u32.bend:133

import Base

133law to_nat_inj:
134  for +a: U32
135  for +b: U32
136  for +h: {U32.to_nat(a) == U32.to_nat(b) : Nat}
137  {a == b : U32}