PROOF.strans.step: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 4076-4106 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=4076&end_line=4106

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

# One step of transitivity on the heads a < b < c, with the tails' result as ih.
def strans.step(
  +a: U32, +b: U32, +c: U32, -s: String, -t: String, -u: String, c1: Cmp, c2: Cmp,
  h1: {U32.cmp(a, b) == c1 : Cmp}, h2: {U32.cmp(b, c) == c2 : Cmp},
  e1: {Order.string.fin(c1, Order.string(s, t)) == LT{} : Cmp},
  e2: {Order.string.fin(c2, Order.string(t, u)) == LT{} : Cmp},
  ih: {Order.string(s, t) == LT{} : Cmp} -> {Order.string(t, u) == LT{} : Cmp} -> {Order.string(s, u) == LT{} : Cmp}
) -> {Order.string.fin(U32.cmp(a, c), Order.string(s, u)) == LT{} : Cmp}:
  match c1 c2:
    case LT{} LT{}:
      %Equal.sym(Cmp, U32.cmp(a, c), LT{}, ucmp_trans(a, b, c, h1, h2)) : {Order.string.fin(_, Order.string(s, u)) == LT{} : Cmp}
      {==}
    case LT{} EQ{}:
      +ebc = ucmp_eq(b, c, h2)
      +eac = rw(U32, w => {U32.cmp(a, w) == LT{} : Cmp}, c, b, Equal.sym(U32, b, c, ebc), h1)
      %Equal.sym(Cmp, U32.cmp(a, c), LT{}, eac) : {Order.string.fin(_, Order.string(s, u)) == LT{} : Cmp}
      {==}
    case EQ{} LT{}:
      +eab = ucmp_eq(a, b, h1)
      +eac = rw(U32, w => {U32.cmp(w, c) == LT{} : Cmp}, a, b, eab, h2)
      %Equal.sym(Cmp, U32.cmp(a, c), LT{}, eac) : {Order.string.fin(_, Order.string(s, u)) == LT{} : Cmp}
      {==}
    case EQ{} EQ{}:
      +eca = Equal.sym(U32, a, c, Equal.trans(U32, a, b, c, ucmp_eq(a, b, h1), ucmp_eq(b, c, h2)))
      +eac = rw(U32, w => {U32.cmp(a, w) == EQ{} : Cmp}, c, a, eca, ucmp_refl(a))
      %Equal.sym(Cmp, U32.cmp(a, c), EQ{}, eac) : {Order.string.fin(_, Order.string(s, u)) == LT{} : Cmp}
      ih(e1, e2)
    case GT{} _:
      lt_absurd({Order.string.fin(U32.cmp(a, c), Order.string(s, u)) == LT{} : Cmp}, GT{}, {==}, e1)
    case _ GT{}:
      lt_absurd({Order.string.fin(U32.cmp(a, c), Order.string(s, u)) == LT{} : Cmp}, GT{}, {==}, e2)

Uses (13):
  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=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=lt_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=rw
  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/PROOF.bend&name=ucmp_refl
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=ucmp_trans
  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