def internal_length_append

bend-mathlib@0.8.1.0 · string.bend:53

import Base

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