U32.from_nat_step: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend as U32
Lines 80-83 of bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/u32.bend&start_line=80&end_line=83

import Base

# the U32 step over abstract words a (for p) and b (for p + 1)
def from_nat_step(+p: Nat, +a: Word(32n), +b: Word(32n), +rec: {U32.from_nat(p) == U32{a} : U32}, +hinc: {Word.inc(32n, a) == b : Word(32n)}) -> {U32.from_nat(1n+p) == U32{b} : U32}:
  %Equal.sym(U32, U32.from_nat(p), U32{a}, rec) : {U32.inc(_) == U32{b} : U32}
  Equal.cong(Word(32n), U32, w => U32{w}, Word.inc(32n, a), b, hinc)

Uses (8):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.inc