law sv_m

lawful-bytes@0.1.1.0 · proof_shift.bend:208

import lawful-bytes@0.1.1.0/proof_shift.bend as ProofShift

import Base

208law sv_m:
209  for +jj: Nat
210  for +kk: Nat
211  for +n: Nat
212  {Nat.add(Nat.add(Nat.add(jj, 1n), kk), n) == Nat.add(Nat.add(jj, kk), 1n+n) : Nat}

Uses (5)

Used by (1)

lawful-bytes@0.1.1.0/proof_shift:sv