PROOF.seq.step: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 4023-4039 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=4023&end_line=4039

import Base
import bend-kit-collections@0.1.4.1/order.bend as Order

# One step of eq on the heads a and b, with the tails' result as ih.
def seq.step(
  +a: U32, +b: U32, +s: String, +t: String, c: Cmp, h: {U32.cmp(a, b) == c : Cmp},
  e: {Order.string.fin(c, Order.string(s, t)) == EQ{} : Cmp},
  ih: {Order.string(s, t) == EQ{} : Cmp} -> {s == t : String}
) -> {SCon{Chr{a}, s} == SCon{Chr{b}, t} : String}:
  match c:
    case LT{}:
      ne_absurd({SCon{Chr{a}, s} == SCon{Chr{b}, t} : String}, LT{}, {==}, e)
    case EQ{}:
      +ea = ucmp_eq(a, b, h)
      +es = ih(e)
      %ea : {SCon{Chr{a}, s} == SCon{Chr{_}, t} : String}
      %es : {SCon{Chr{a}, s} == SCon{Chr{a}, _} : String}
      {==}
    case GT{}:
      ne_absurd({SCon{Chr{a}, s} == SCon{Chr{b}, t} : String}, GT{}, {==}, e)

Uses (9):
  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=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.cmp
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=ne_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=ucmp_eq
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/order.bend&name=string
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/order.bend&name=string.fin