∀ {pat s : ByteArray} {stackPos needlePos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos →
    ∀ newStackPos ≤ stackPos,
      stackPos - newStackPos ≤ needlePos →
        String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝¹ pat s (needlePos - (stackPos - newStackPos))
          newStackPos