IndexProofs.flatten_unflatten_step: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as IndexProofs
Lines 118-121 of bendtorch-core@0.1.0.0/src/shape/index_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&start_line=118&end_line=121

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

def flatten_unflatten_step(+head: Nat, +tail: List<&2, Nat>, rec: @+index: Shape.Fin(Shape.numel(tail)) -> {Shape.flatten(tail, Shape.unflatten(tail, index)) == index : Shape.Fin(Shape.numel(tail))}, coordinate: Shape.Fin(head) & Shape.Fin(Shape.numel(tail))) -> {Shape.flatten(head <> tail, Shape.unflatten.step(head, tail, rest => Shape.unflatten(tail, rest), coordinate)) == Shape.Fin.pack(head, Shape.numel(tail), coordinate) : Shape.Fin(Shape.numel(head <> tail))}:
  (first, +last) = coordinate
  %rec(last) : {Shape.Fin.pack(head, Shape.numel(tail), (first, Shape.flatten(tail, Shape.unflatten(tail, last)))) == Shape.Fin.pack(head, Shape.numel(tail), (first, _)) : Shape.Fin(Shape.numel(head <> tail))}
  {==}

Uses (10):
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.pack
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=flatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten.step