law allz_cmp

lawful-words@0.1.0.0 · proof_zb.bend:40

import Base

40law allz_cmp:
41  for +n: Nat
42  for +w: Word(n)
43  {Cmp.is_eq(Word.cmp(n, w, Word.zero(n))) == allz(n, w) : Bool}