{s : String.Slice} →
  {P : Sort u} →
    {pos : s.Pos} →
      {h : pos ≠ s.endPos} →
        {pos' : s.Pos} →
          {h' : pos' ≠ s.endPos} →
            String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h =
                String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos' h' →
              (pos ≍ pos' → P) → P