law word_to_nat_inj

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

import Base

234# Two words with the same value are the same word.
235law word_to_nat_inj:
236  for n: Nat
237  for a: Word(n)
238  for b: Word(n)
239  for h: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
240  {a == b : Word(n)}