law winj

lawful-words@0.1.0.0 · proof_word.bend:295

import Base

295# Two words that stand for the same number are the same word.
296law winj:
297  for +n: Nat
298  for +a: Word(n)
299  for +b: Word(n)
300  for +e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
301  {a == b : Word(n)}