law add_succ
import lawful-arrays@0.1.0.0/proof_base.bend as ProofBaseimport Base
112law add_succ:
113 for +a: Nat
114 for +b: Nat
115 {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}
import lawful-arrays@0.1.0.0/proof_base.bend as ProofBaseimport Base
112law add_succ:
113 for +a: Nat
114 for +b: Nat
115 {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}