law adc_t

lawful-words@0.1.0.0 · proof_word.bend:464

import Base

464law adc_t:
465  for +n: Nat
466  for +a: Word(n)
467  for +b: Word(n)
468  for +c: Bool
469  {Word.adc(n, a, b, True{}, c) == Word.adc(n, a, Word.not(n, b), False{}, c) : Word(n)}