∀ {pat s : ByteArray} {stackPos needlePos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s (needlePos + 1) (stackPos + 1) ↔
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos ∧
      ∃ (h₁ : needlePos < pat.size) (h₂ : stackPos < s.size), pat[needlePos] = s[stackPos]