TraversalBatchRefinement.last_step: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as TraversalBatchRefinement
Lines 27-32 of stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&start_line=27&end_line=32

import Base
import stelliferous@0.0.2.0/traversal_loop.bend as Loop

# A loop's last step, for every state and count.
def last_step(~State: Data,~step: State -> State,+count: Nat,+state: State) ->
  {Loop.run(~State,~step,1n+count,state) == step(Loop.run(~State,~step,count,state)) : State}:
  match count:
    case 0n: {==}
    case 1n+ +rest: last_step(~State,~step,rest,step(state))

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_loop.bend&name=run