(motive : List Char → String.Pos.Raw → String.Pos.Raw → Sort u_1) →
  (x : List Char) →
    (x_1 x_2 : String.Pos.Raw) →
      ((x x_3 : String.Pos.Raw) → motive [] x x_3) →
        ((c : Char) → (cs : List Char) → (i p : String.Pos.Raw) → motive (c :: cs) i p) → motive x x_1 x_2