no goals
α : Type u_1
l m r : List Char
f : α → Char → α
init : α
⊢ Substring.foldl f init
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } } =
    List.foldl f init m
simp [-List.append_assoc, Substring.foldl, foldlAux_of_valid]