law add_succ

bend-collections@1.0.0.0 · proofs/crypto/sha/list_proofs.bend:45

import Base

45law add_succ:
46  for n: Nat
47  for m: Nat
48  {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}