∀ (s : String.Slice) (currPos : s.Pos) (needle : Char → Bool) (h1 : ¬currPos = s.startPos),
  needle ((currPos.prev h1).get ⋯) = true →
    match
      Std.IterStep.yield { internalState := { currPos := currPos.prev h1, needle := needle } }
        (String.Slice.Pattern.SearchStep.matched (currPos.prev h1) currPos) with
    | Std.IterStep.yield it' out =>
      { internalState := { currPos := currPos, needle := needle } }.internalState.needle = it'.internalState.needle ∧
        ∃ (h1 : { internalState := { currPos := currPos, needle := needle } }.internalState.currPos ≠ s.startPos),
          it'.internalState.currPos =
              { internalState := { currPos := currPos, needle := needle } }.internalState.currPos.prev h1 ∧
            match out with
            | String.Slice.Pattern.SearchStep.matched startPos endPos =>
              { internalState := { currPos := currPos, needle := needle } }.internalState.currPos = endPos ∧
                it'.internalState.currPos = startPos ∧
                  { internalState := { currPos := currPos, needle := needle } }.internalState.needle
                      (({ internalState := { currPos := currPos, needle := needle } }.internalState.currPos.prev h1).get
                        ⋯) =
                    true
            | String.Slice.Pattern.SearchStep.rejected startPos endPos =>
              { internalState := { currPos := currPos, needle := needle } }.internalState.currPos = endPos ∧
                it'.internalState.currPos = startPos ∧
                  ¬{ internalState := { currPos := currPos, needle := needle } }.internalState.needle
                        (({ internalState := { currPos := currPos, needle := needle } }.internalState.currPos.prev
                              h1).get
                          ⋯) =
                      true
    | Std.IterStep.skip it => False
    | Std.IterStep.done =>
      { internalState := { currPos := currPos, needle := needle } }.internalState.currPos = s.startPos