{s : String.Slice} →
  {P : Sort u} →
    {startPos endPos startPos' endPos' : s.Pos} →
      String.Slice.Pattern.SearchStep.rejected startPos endPos =
          String.Slice.Pattern.SearchStep.rejected startPos' endPos' →
        (startPos ≍ startPos' → endPos ≍ endPos' → P) → P