law Bq.Nat.add_succ

import gralha-bendquest@0.1.0.0/game.bend as Game

import Base

676law Bq.Nat.add_succ:
677  (@+a_0: Nat -> (@+b_1: Nat -> {Bq.Nat.add(a_0, Succ{b_1}) == Succ{Bq.Nat.add(a_0, b_1)} : Nat}))

Uses (3)