-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.instIteratorId.match_1.eq_4 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice}
  (motive : Std.IterM Id String.Slice → Std.IterStep (Std.IterM Id String.Slice) String.Slice → 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 : String.Slice) →
              motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_2 }
                (Std.IterStep.yield { internalState := String.Slice.SplitInclusiveIterator.operating currPos_1 s' }
                  out))
  (h_2 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        (out : String.Slice) →
          motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_2 }
            (Std.IterStep.yield { internalState := String.Slice.SplitInclusiveIterator.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.SplitInclusiveIterator.operating currPos s_2 }
              (Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.operating currPos_1 s' }))
  (h_4 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_2 }
          (Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.atEnd }))
  (h_5 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_2 } Std.IterStep.done)
  (h_6 :
    (it : Std.IterM Id String.Slice) →
      (out : String.Slice) →
        motive { internalState := String.Slice.SplitInclusiveIterator.atEnd } (Std.IterStep.yield it out))
  (h_7 :
    (it : Std.IterM Id String.Slice) →
      motive { internalState := String.Slice.SplitInclusiveIterator.atEnd } (Std.IterStep.skip it))
  (h_8 : Unit → motive { internalState := String.Slice.SplitInclusiveIterator.atEnd } Std.IterStep.done),
  (match { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_1 },
      Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.atEnd } with
    | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_2 },
      Std.IterStep.yield { internalState := String.Slice.SplitInclusiveIterator.operating currPos_1 s' } out =>
      h_1 currPos s_2 currPos_1 s' out
    | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s },
      Std.IterStep.yield { internalState := String.Slice.SplitInclusiveIterator.atEnd } out => h_2 currPos s out
    | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s_2 },
      Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.operating currPos_1 s' } =>
      h_3 currPos s_2 currPos_1 s'
    | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s },
      Std.IterStep.skip { internalState := String.Slice.SplitInclusiveIterator.atEnd } => h_4 currPos s
    | { internalState := String.Slice.SplitInclusiveIterator.operating currPos s }, Std.IterStep.done => h_5 currPos s
    | { internalState := String.Slice.SplitInclusiveIterator.atEnd }, Std.IterStep.yield it out => h_6 it out
    | { internalState := String.Slice.SplitInclusiveIterator.atEnd }, Std.IterStep.skip it => h_7 it
    | { internalState := String.Slice.SplitInclusiveIterator.atEnd }, Std.IterStep.done => h_8 ()) =
    h_4 currPos s_1