∀ {pat s : String.Slice} {needlePos stackPos : String.Pos.Raw},
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants✝ pat s needlePos stackPos →
    needlePos = 0 → String.Pos.Raw.IsValidForSlice s stackPos