∀ (s : String.Slice) (motive : String.Slice.Pattern.ForwardSliceSearcher s → Sort u_1) (needle : String.Slice)
  (table : Vector ℕ needle.utf8ByteSize) (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle)
  (stackPos needlePos : String.Pos.Raw) (hn : needlePos < needle.rawEndPos)
  (h_1 : (pos : s.Pos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos))
  (h_2 : (pos : s.Pos) → (h : pos ≠ s.endPos) → motive (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h))
  (h_3 :
    (needle : String.Slice) →
      (table : Vector ℕ needle.utf8ByteSize) →
        (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) →
          (stackPos needlePos : String.Pos.Raw) →
            (hn : needlePos < needle.rawEndPos) →
              motive (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn))
  (h_4 : Unit → motive String.Slice.Pattern.ForwardSliceSearcher.atEnd),
  (match String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn with
    | String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos => h_1 pos
    | String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h => h_2 pos h
    | String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =>
      h_3 needle table ht stackPos needlePos hn
    | String.Slice.Pattern.ForwardSliceSearcher.atEnd => h_4 ()) =
    h_3 needle table ht stackPos needlePos hn