∀ {ρ : Type} (pat : ρ) (s : String.Slice) [inst : String.Slice.Pattern.BackwardPattern pat]
  (it : Std.IterM Id (String.Slice.Pattern.SearchStep s)),
  it.internalState.currPos = s.startPos →
    match Std.IterStep.done with
    | Std.IterStep.yield it' (String.Slice.Pattern.SearchStep.rejected p₁ p₂) =>
      ∃ (h : it.internalState.currPos ≠ s.startPos),
        String.Slice.Pattern.BackwardPattern.dropSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) ⋯ = none ∧
          p₁ = it.internalState.currPos.prev h ∧
            p₂ = it.internalState.currPos ∧ it'.internalState.currPos = it.internalState.currPos.prev h
    | Std.IterStep.yield it' (String.Slice.Pattern.SearchStep.matched p₁ p₂) =>
      ∃ (h : it.internalState.currPos ≠ s.startPos),
        ∃ pos,
          String.Slice.Pattern.BackwardPattern.dropSuffixOfNonempty? pat (s.sliceTo it.internalState.currPos) ⋯ =
              some pos ∧
            p₁ = String.Slice.Pos.ofSliceTo pos ∧
              p₂ = it.internalState.currPos ∧ it'.internalState.currPos = String.Slice.Pos.ofSliceTo pos
    | Std.IterStep.done => it.internalState.currPos = s.startPos
    | Std.IterStep.skip it => False