∀ {l m r : List Char}
  (motive :
    (x : Substring.Raw) →
      x.str.toList = l ++ m ++ r →
        x.startPos.byteIdx = String.utf8Len l → x.stopPos.byteIdx = String.utf8Len l + String.utf8Len m → Prop)
  (x : Substring.Raw) (x_1 : x.str.toList = l ++ m ++ r) (x_2 : x.startPos.byteIdx = String.utf8Len l)
  (x_3 : x.stopPos.byteIdx = String.utf8Len l + String.utf8Len m),
  (∀ (s : String)
      (h :
        { str := s, startPos := { byteIdx := String.utf8Len l },
                stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } }.str.toList =
          l ++ m ++ r),
      motive
        { str := s, startPos := { byteIdx := String.utf8Len l },
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len m } }
        h ⋯ ⋯) →
    motive x x_1 x_2 x_3