∀ {l ml mm mr r : List Char}
  (motive :
    (e b : String.Pos.Raw) →
      (x : Substring.Raw) →
        Substring.Raw.ValidFor l (ml ++ mm ++ mr) r x →
          Substring.Raw.ValidFor ml mm mr { str := String.ofList (ml ++ mm ++ mr), startPos := b, stopPos := e } → Prop)
  (e b : String.Pos.Raw) (x : Substring.Raw) (x_1 : Substring.Raw.ValidFor l (ml ++ mm ++ mr) r x)
  (x_2 : Substring.Raw.ValidFor ml mm mr { str := String.ofList (ml ++ mm ++ mr), startPos := b, stopPos := e }),
  (∀ (a : Unit),
      motive { byteIdx := String.utf8Len ml + String.utf8Len mm } { byteIdx := String.utf8Len ml }
        { str := String.ofList (l ++ (ml ++ mm ++ mr) ++ r), startPos := { byteIdx := String.utf8Len l },
          stopPos := { byteIdx := String.utf8Len l + String.utf8Len (ml ++ mm ++ mr) } }
        ⋯ ⋯) →
    motive e b x x_1 x_2