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

import Base

def internal_length_append(a: String, -b: String) -> {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}:
  match a:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      %internal_length_append(t, b) : {1n+Nat.add(String.length(t), String.length(b)) == 1n+_ : Nat}
      {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.length