CoordinateProofs.fits_of.step: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as CoordinateProofs
Lines 115-120 of bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&start_line=115&end_line=120

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

def fits_of.step(-dh: Nat, -dt: List<&2, Nat>, -vh: Nat, -vt: List<&2, Nat>, verdict: Shape.BoolCase<Nat.is_lt(vh, dh)>, ok: {True{} == Bool.and(Nat.is_lt(vh, dh), Shape.fit(dt, vt)) : Bool}, rec: {True{} == Shape.fit(dt, vt) : Bool} -> Fits(dt, vt)) -> Fits(dh <> dt, vh <> vt):
  match verdict:
    case Shape.BFalse{equal}:
      Empty.absurd(Fits(dh <> dt, vh <> vt), Shape.clash(Equal.trans(Bool, True{}, Bool.and(Nat.is_lt(vh, dh), Shape.fit(dt, vt)), False{}, ok, Equal.cong(Bool, Bool, head => Bool.and(head, Shape.fit(dt, vt)), Nat.is_lt(vh, dh), False{}, Equal.sym(Bool, False{}, Nat.is_lt(vh, dh), equal)))))
    case Shape.BTrue{+equal}:
      FStep{equal, rec(Equal.trans(Bool, True{}, Bool.and(Nat.is_lt(vh, dh), Shape.fit(dt, vt)), Shape.fit(dt, vt), ok, Equal.cong(Bool, Bool, head => Bool.and(head, Shape.fit(dt, vt)), Nat.is_lt(vh, dh), True{}, Equal.sym(Bool, True{}, Nat.is_lt(vh, dh), equal))))}

Uses (14):
  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=Empty.absurd
  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=Equal.trans
  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/shape/coordinate_proofs.bend&name=Fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=Fits.Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=fit