IndexProofs.unpack_pack: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as IndexProofs
Lines 84-96 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=84&end_line=96

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

def unpack_pack(+a: Nat, +b: Nat, +first: Shape.Fin(a), +last: Shape.Fin(b)) -> {Shape.Fin.unpack(a, b, Shape.Fin.pack(a, b, (first, last))) == (first, last) : Shape.Fin(a) & Shape.Fin(b)}:
  match a:
    case 0n:
      match first:
    case 1n+p:
      match first:
        case Shape.FZero{}:
          %split_left(b, Nat.mul(p, b), last) : {Shape.Fin.unpack.step(p, b, index => Shape.Fin.unpack(p, b, index), Shape.Fin.split(b, Nat.mul(p, b), Shape.Fin.left(b, Nat.mul(p, b), last))) == Shape.Fin.unpack.step(p, b, index => Shape.Fin.unpack(p, b, index), _) : Shape.Fin(1n+p) & Shape.Fin(b)}
          {==}
        case Shape.FNext{+previous}:
          %unpack_pack(p, b, previous, last) : {Shape.Fin.unpack(1n+p, b, Shape.Fin.pack(1n+p, b, (Shape.FNext{previous}, last))) == Shape.Fin.unpack.lift(p, b, _) : Shape.Fin(1n+p) & Shape.Fin(b)}
          %split_shift(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last))) : {Shape.Fin.unpack.step(p, b, index => Shape.Fin.unpack(p, b, index), Shape.Fin.split(b, Nat.mul(p, b), Shape.Fin.shift(b, Nat.mul(p, b), Shape.Fin.pack(p, b, (previous, last))))) == Shape.Fin.unpack.step(p, b, index => Shape.Fin.unpack(p, b, index), _) : Shape.Fin(1n+p) & Shape.Fin(b)}
          {==}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  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.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.left
  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=Fin.shift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.split
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.unpack
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.unpack.lift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.unpack.step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=split_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=split_shift