{σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} →
        [inst : String.Slice.Pattern.ToBackwardSearcher pat σ] →
          {motive : String.Slice.RevSplitIterator pat s → Sort u} →
            (t : String.Slice.RevSplitIterator pat s) →
              t.ctorIdx = 1 → motive String.Slice.RevSplitIterator.atEnd → motive t