law zero_reflect

stelliferous@0.0.2.0 · proofs/word_encoding.bend:230

import Base

230law zero_reflect:
231  for +n: Nat
232  for +w: Word(n)
233  for eq: {Word.cmp(n,w,Word.zero(n)) == EQ{} : Cmp}
234  {w == Word.zero(n) : Word(n)}