Fixbytes.step32: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend as Fixbytes
Lines 78-83 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&start_line=78&end_line=83

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as P32

def step32(+k: Nat, +hk: {Nat.is_le(Nat.add(8n, k), 32n) == True{} : Bool}, +z: U32, +hz: {C.fits(k, v(z)) == True{} : Bool}, +b: U32, +hb: {C.fits(8n, v(b)) == True{} : Bool}) -> {v(U32.add(b, U32.mul(z, 256))) == Nat.add(v(b), C.shift(8n, v(z))) : Nat}:
  +sz = C.shift(8n, v(z))
  +f0 = Equal.trans(Bool, C.fits(32n, sz), C.fits(32n, Nat.add(0n, sz)), True{}, Equal.cong(Nat, Bool, t => C.fits(32n, t), sz, Nat.add(0n, sz), Equal.sym(Nat, Nat.add(0n, sz), sz, P32.zero_add(sz))), to32(k, hk, Nat.add(0n, sz), step_fits(k, 0n, v(z), {==}, hz)))
  +em = Equal.trans(Nat, v(U32.mul(z, 256)), C.low(32n, Nat.mul(v(z), 256n)), sz, P32.mul_low(z, 256), Equal.trans(Nat, C.low(32n, Nat.mul(v(z), 256n)), C.low(32n, sz), sz, Equal.cong(Nat, Nat, t => C.low(32n, t), Nat.mul(v(z), 256n), sz, Equal.sym(Nat, sz, Nat.mul(v(z), 256n), WW.shift_mul(8n, v(z)))), WW.low_fit(32n, sz, f0)))
  +ea = Equal.trans(Nat, v(U32.add(b, U32.mul(z, 256))), C.low(32n, Nat.add(v(b), v(U32.mul(z, 256)))), C.low(32n, Nat.add(v(b), sz)), P32.add_low(b, U32.mul(z, 256)), Equal.cong(Nat, Nat, t => C.low(32n, Nat.add(v(b), t)), v(U32.mul(z, 256)), sz, em))
  Equal.trans(Nat, v(U32.add(b, U32.mul(z, 256))), C.low(32n, Nat.add(v(b), sz)), Nat.add(v(b), sz), ea, WW.low_fit(32n, Nat.add(v(b), sz), to32(k, hk, Nat.add(v(b), sz), step_fits(k, v(b), v(z), hb, hz))))

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend&name=add_low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend&name=mul_low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend&name=zero_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=step_fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=to32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixbytes.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_fit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=shift_mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift