BoundaryProofs.fin_of_value: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
Lines 30-39 of bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&start_line=30&end_line=39

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

def fin_of_value(+bound: Nat, +index: Shape.Fin(bound)) -> {Some{index} == Laws.fin_of(bound, Shape.Fin.value(bound, index)) : Maybe<&2, Shape.Fin(bound)>}:
  match bound:
    case 0n:
      match index:
    case 1n+p:
      match index:
        case Shape.FZero{}:
          {==}
        case Shape.FNext{+previous}:
          Equal.cong(Maybe<&2, Shape.Fin(p)>, Maybe<&2, Shape.Fin(1n+p)>, index => Laws.fin_of.next(p, index), Some{previous}, Laws.fin_of(p, Shape.Fin.value(p, previous)), fin_of_value(p, previous))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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/shape/LAWS.bend&name=fin_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=fin_of.next
  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.value