law word_to_nat_inj

bend-mathlib@0.8.1.0 · u32.bend:50

import Base

50# Distinct words have distinct values: to_nat a = to_nat b implies a = b.
51law word_to_nat_inj:
52  for n: Nat
53  for a: Word(n)
54  for b: Word(n)
55  for e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
56  {a == b : Word(n)}