def internal_cmp_rec_snd

bend-mathlib@0.8.1.0 · string.bend:209

import Base

209def internal_cmp_rec_snd(h1: Char, h2: Char, rr: (String & String) & Cmp) -> {Pair.snd(String & String, Cmp, String.cmp.rec(h1, h2, rr)) == Pair.snd(String & String, Cmp, rr) : Cmp}:
210  match rr:
211    case (ts, r):
212      match ts:
213        case (t1, t2):
214          {==}