law to_nat_inj

lawful-words@0.1.0.0 · LAWS.bend:21

import Base

21# Two words that stand for the same number are the same word.
22law to_nat_inj:
23  for a: U32
24  for b: U32
25  for h: {U32.to_nat(a) == U32.to_nat(b) : Nat}
26  {a == b : U32}