ReduceParallelProof.kept_below: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof
Lines 198-206 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=198&end_line=206

import Base
import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber

def kept_below(+keep: Bool, +position: Nat, +rest: List<&2, Nat>, +bound: Nat,
  +inside: {Nat.is_lt(position, bound) == True{} : Bool}, +others: {all_below(rest, bound) == True{} : Bool}) ->
  {all_below(Fiber.kept(keep, position, rest), bound) == True{} : Bool}:
  match keep:
    case True{}:
      %Equal.sym(Bool, Nat.is_lt(position, bound), True{}, inside) : {Bool.and(_, all_below(rest, bound)) == True{} : Bool}
      others
    case False{}:
      others

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  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=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=all_below