law inc_left

stelliferous@0.0.2.0 · proofs/word_arithmetic.bend:28

import Base

28law inc_left:
29  for +n: Nat
30  for +a: Word(n)
31  for +b: Word(n)
32  {Word.add(n,Word.inc(n,a),b) == Word.inc(n,Word.add(n,a,b)) : Word(n)}