{σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} →
        [inst : String.Slice.Pattern.ToBackwardSearcher pat σ] →
          {motive : String.Slice.RevSplitIterator pat s → Sort u} →
            ((currPos : s.Pos) →
                (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                  motive (String.Slice.RevSplitIterator.operating currPos searcher)) →
              motive String.Slice.RevSplitIterator.atEnd → (t : String.Slice.RevSplitIterator pat s) → motive t