String.internal_order_step: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/string.bend as String
Lines 216-223 of bend-mathlib@0.8.1.0/string.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/string.bend&start_line=216&end_line=223

import Base

def internal_order_step(+t1: String, +t2: String, h1: Char, h2: Char, c: Cmp, ih: {String.order.go(t1, t2, EQ{}) == Pair.snd(String & String, Cmp, String.cmp(t1, t2)) : Cmp}) -> {String.order.go(t1, t2, c) == Pair.snd(String & String, Cmp, String.cmp.fin(t1, t2, ((h1, h2), c))) : Cmp}:
  match c:
    case LT{}:
      internal_order_go_lt(t1, t2)
    case EQ{}:
      Equal.trans(Cmp, String.order.go(t1, t2, EQ{}), Pair.snd(String & String, Cmp, String.cmp(t1, t2)), Pair.snd(String & String, Cmp, String.cmp.rec(h1, h2, String.cmp(t1, t2))), ih, Equal.sym(Cmp, Pair.snd(String & String, Cmp, String.cmp.rec(h1, h2, String.cmp(t1, t2))), Pair.snd(String & String, Cmp, String.cmp(t1, t2)), internal_cmp_rec_snd(h1, h2, String.cmp(t1, t2))))
    case GT{}:
      internal_order_go_gt(t1, t2)

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.cmp.rec
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.order.go
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/string.bend&name=internal_cmp_rec_snd
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/string.bend&name=internal_order_go_gt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/string.bend&name=internal_order_go_lt