∀ {s : String.Slice} (needle : String.Slice) (table : Vector ℕ needle.utf8ByteSize)
  (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) (stackPos needlePos : String.Pos.Raw)
  (hn : needlePos < needle.rawEndPos) (needle_1 : String.Slice) (table_1 : Vector ℕ needle_1.utf8ByteSize)
  (ht_1 : table_1 = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle_1)
  (stackPos_1 needlePos_1 : String.Pos.Raw) (hn_1 : needlePos_1 < needle_1.rawEndPos),
  (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn =
      String.Slice.Pattern.ForwardSliceSearcher.proper needle_1 table_1 ht_1 stackPos_1 needlePos_1 hn_1) =
    (needle = needle_1 ∧ table ≍ table_1 ∧ stackPos = stackPos_1 ∧ needlePos = needlePos_1)