∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : Std.IterM Id s.Subslice → Std.IterStep (Std.IterM Id s.Subslice) s.Subslice → Sort u_1)
  (currPos : s.Pos) (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (currPos_1 : s.Pos) →
          (s' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
            (out : s.Subslice) →
              motive { internalState := String.Slice.SplitIterator.operating currPos s_2 }
                (Std.IterStep.yield { internalState := String.Slice.SplitIterator.operating currPos_1 s' } out))
  (h_2 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (out : s.Subslice) →
          motive { internalState := String.Slice.SplitIterator.operating currPos s_2 }
            (Std.IterStep.yield { internalState := String.Slice.SplitIterator.atEnd } out))
  (h_3 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (currPos_1 : s.Pos) →
          (s' : Std.Iter (String.Slice.Pattern.SearchStep s)) →
            motive { internalState := String.Slice.SplitIterator.operating currPos s_2 }
              (Std.IterStep.skip { internalState := String.Slice.SplitIterator.operating currPos_1 s' }))
  (h_4 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.SplitIterator.operating currPos s_2 }
          (Std.IterStep.skip { internalState := String.Slice.SplitIterator.atEnd }))
  (h_5 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.SplitIterator.operating currPos s_2 } Std.IterStep.done)
  (h_6 :
    (it : Std.IterM Id s.Subslice) →
      (out : s.Subslice) → motive { internalState := String.Slice.SplitIterator.atEnd } (Std.IterStep.yield it out))
  (h_7 :
    (it : Std.IterM Id s.Subslice) →
      motive { internalState := String.Slice.SplitIterator.atEnd } (Std.IterStep.skip it))
  (h_8 : Unit → motive { internalState := String.Slice.SplitIterator.atEnd } Std.IterStep.done),
  (match { internalState := String.Slice.SplitIterator.operating currPos s_1 }, Std.IterStep.done with
    | { internalState := String.Slice.SplitIterator.operating currPos s_2 },
      Std.IterStep.yield { internalState := String.Slice.SplitIterator.operating currPos_1 s' } out =>
      h_1 currPos s_2 currPos_1 s' out
    | { internalState := String.Slice.SplitIterator.operating currPos s_2 },
      Std.IterStep.yield { internalState := String.Slice.SplitIterator.atEnd } out => h_2 currPos s_2 out
    | { internalState := String.Slice.SplitIterator.operating currPos s_2 },
      Std.IterStep.skip { internalState := String.Slice.SplitIterator.operating currPos_1 s' } =>
      h_3 currPos s_2 currPos_1 s'
    | { internalState := String.Slice.SplitIterator.operating currPos s },
      Std.IterStep.skip { internalState := String.Slice.SplitIterator.atEnd } => h_4 currPos s
    | { internalState := String.Slice.SplitIterator.operating currPos s }, Std.IterStep.done => h_5 currPos s
    | { internalState := String.Slice.SplitIterator.atEnd }, Std.IterStep.yield it out => h_6 it out
    | { internalState := String.Slice.SplitIterator.atEnd }, Std.IterStep.skip it => h_7 it
    | { internalState := String.Slice.SplitIterator.atEnd }, Std.IterStep.done => h_8 ()) =
    h_5 currPos s_1