def internal_order_step
bend-mathlib@0.8.1.0 · string.bend:216
import bend-mathlib@0.8.1.0/string.bend as String
import Base
216def 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}:
217 match c:
218 case LT{}:
219 internal_order_go_lt(t1, t2)
220 case EQ{}:
221 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))))
222 case GT{}:
223 internal_order_go_gt(t1, t2)