String.internal_cmp_refl: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/string.bend as String
Lines 167-176 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=167&end_line=176

import Base

def internal_cmp_refl(s: String) -> {((s, s), EQ{}) == String.cmp(s, s) : (String & String) & Cmp}:
  match s:
    case SNil{}:
      {==}
    case SCon{h, t}:
      match h:
        case Chr{x}:
          %internal_u32_cmp_refl(x) : {((SCon{Chr{x}, t}, SCon{Chr{x}, t}), EQ{}) == String.cmp.fin(t, t, ((Chr{x}, Chr{x}), _)) : (String & String) & Cmp}
          %internal_cmp_refl(t) : {((SCon{Chr{x}, t}, SCon{Chr{x}, t}), EQ{}) == String.cmp.rec(Chr{x}, Chr{x}, _) : (String & String) & Cmp}
          {==}

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=Pair
  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=bend-mathlib@0.8.1.0/string.bend&name=internal_u32_cmp_refl