law add11

lawful-bytes@0.1.1.0 · proof_find.bend:93

import Base

93# (j + 1) + 1 is j + 2, for every word j (no range needed: through from_nat).
94law add11:
95  for +j: U32
96  {U32.add(U32.add(j, 1), 1) == U32.add(j, 2) : U32}