ReduceFiberProof.rest_at: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 647-660 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=647&end_line=660

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

# ... and so at every base.
def rest_at(+rest: List<&2, Shape.Row>, +others: List<&2, Nat>, +inner: Nat, +stride: Nat, +walk: RestWalk(rest, others, inner, stride),
  +base: Nat) ->
  {masked(stride, rest, inner, base, 0n) ==
    visited(rest, others, Reduce.first_span(rest, others), inner, base, Reduce.first_digit(rest, inner)) : List<&2, Nat>}:
  %Equal.sym(List<&2, Nat>, masked(stride, rest, inner, base, 0n), shift(base, masked(stride, rest, inner, 0n, 0n)),
    masked_base(stride, rest, inner, base, 0n)) :
    {_ == visited(rest, others, Reduce.first_span(rest, others), inner, base, Reduce.first_digit(rest, inner)) : List<&2, Nat>}
  %Equal.sym(List<&2, Nat>, visited(rest, others, Reduce.first_span(rest, others), inner, base, Reduce.first_digit(rest, inner)),
    shift(base, visited(rest, others, Reduce.first_span(rest, others), inner, 0n, Reduce.first_digit(rest, inner))),
    visited_base(rest, others, Reduce.first_span(rest, others), inner, base, Reduce.first_digit(rest, inner))) :
    {shift(base, masked(stride, rest, inner, 0n, 0n)) == _ : List<&2, Nat>}
  Equal.cong(List<&2, Nat>, List<&2, Nat>, xs => shift(base, xs), masked(stride, rest, inner, 0n, 0n),
    visited(rest, others, Reduce.first_span(rest, others), inner, 0n, Reduce.first_digit(rest, inner)), walk)

Uses (13):
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=first_digit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=first_span
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=RestWalk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked_base
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=visited
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=visited_base
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row