{s : String.Slice} →
  {p₂ : s.Pos} →
    (motive : (x : List s.Subslice) → Option.any (fun x => decide (x.startInclusive = p₂)) x.head? = true → Sort u_1) →
      (x : List s.Subslice) →
        (x_1 : Option.any (fun x => decide (x.startInclusive = p₂)) x.head? = true) →
          ((st : s.Subslice) →
              (sts : List s.Subslice) →
                (h : Option.any (fun x => decide (x.startInclusive = p₂)) (st :: sts).head? = true) →
                  motive (st :: sts) h) →
            motive x x_1