Word.add_comm.arm: law of Base
Import: import Base
Lines 1379-1386 of Base/base.bend: https://jend.leeeet.dev/read.txt?path=Base/base.bend&start_line=1379&end_line=1386

import Base

law Word.add_comm.arm:
  for p  : Nat
  for at : Word(p)
  for bt : Word(p)
  for k  : Bool
  for -h : Bool
  {WCon{h, Word.adc(p, at, bt, False{}, k)}
    == WCon{h, Word.adc(p, bt, at, False{}, k)} : Word.Con<p>}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.adc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.add_comm.go