law add_succ

lawful-words@0.1.0.0 · proof_nat.bend:197

import Base

197law add_succ:
198  for +a: Nat
199  for +b: Nat
200  {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}