∀ (motive : Substring.Raw → ℕ → String.Pos.Raw → Sort u_1) (ss : Substring.Raw) (i : ℕ) (p : String.Pos.Raw)
  (h_1 : (x : Substring.Raw) → (p : String.Pos.Raw) → motive x 0 p)
  (h_2 : (ss : Substring.Raw) → (i : ℕ) → (p : String.Pos.Raw) → motive ss i.succ p),
  (match ss, i.succ, p with
    | x, 0, p => h_1 x p
    | ss, i.succ, p => h_2 ss i p) =
    h_2 ss i p