have : String.get ⟨l ++ (m ++ c :: r)⟩ ⟨String.utf8Len l + String.utf8Len m⟩ = c := by
  have eq₁ : l ++ (m ++ c :: r) = (l ++ m) ++ (c :: r) := by simp
  have eq₂ : String.utf8Len l + String.utf8Len m = String.utf8Len (l ++ m) := by simp
  rw [eq₁, eq₂, String.get_of_valid]
  simp
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this : s.stopPos < s.str.endPos
⊢ ValidFor l (m ++ [c]) r
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos :=
        { byteIdx := String.utf8Len l + String.utf8Len m } +
          { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } }
l m : List Char
c : Char
r : List Char
s : Substring
v : ValidFor l m (c :: r) s
this✝ : s.stopPos < s.str.endPos
this : { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } = c
⊢ ValidFor l (m ++ [c]) r
    { str := { data := l ++ (m ++ c :: r) }, startPos := s.startPos,
      stopPos :=
        { byteIdx := String.utf8Len l + String.utf8Len m } +
          { data := l ++ (m ++ c :: r) }.get { byteIdx := String.utf8Len l + String.utf8Len m } }