law cmp_sound

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/subtle/word.bend:191

import Base

191law cmp_sound:
192  for +n: Nat
193  for +x: Word(n)
194  for +y: Word(n)
195  for +h: {Cmp.is_eq(Word.cmp(n, x, y)) == True{} : Bool}
196  {x == y : Word(n)}