∀ {pat s : String.Slice} {stackPos needlePos : String.Pos.Raw} (it : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h : String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos)
  {table : Vector ℕ pat.utf8ByteSize} {ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable pat}
  {hn : needlePos < pat.rawEndPos},
  it = { internalState := String.Slice.Pattern.ForwardSliceSearcher.proper pat table ht stackPos needlePos hn } →
    ∀ {p : s.Pos},
      p = String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base✝ h →
        String.Slice.Pattern.Model.IsValidSearchFrom pat p it.toList