law wext

lawful-words@0.1.0.0 · proof_word.bend:934

import Base

934# Two words with the same bit where they would first differ are equal.
935law wext:
936  for +n: Nat
937  for +a: Word(n)
938  for +b: Word(n)
939  for +e: {wbit(n, a, wdiff(n, a, b)) == wbit(n, b, wdiff(n, a, b)) : Bool}
940  {a == b : Word(n)}