law Bq.stat_succ

gralha-bendquest@0.1.0.0 · game.bend:1004

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

1004law Bq.stat_succ:
1005  (@+a_0: Nat -> (@+b_1: Nat -> (@+c_2: Nat -> (@+d_3: Nat -> {Bq.Nat.add(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, Succ{d_3}))) == Succ{Bq.Nat.add(a_0, Bq.Nat.add(b_1, Bq.Nat.add(c_2, d_3)))} : Nat}))))

Uses (4)

Used by (1)