∀ {pat s : ByteArray} {stackPos needlePos : ℕ}
  (motive :
    (String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos ∧
        ∃ (h₁ : needlePos < pat.size) (h₂ : stackPos < s.size), pat[needlePos] = s[stackPos]) →
      Prop)
  (x :
    String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝¹ pat s needlePos stackPos ∧
      ∃ (h₁ : needlePos < pat.size) (h₂ : stackPos < s.size), pat[needlePos] = s[stackPos]),
  (∀ (h₁ : stackPos ≤ s.size) (h₂ : needlePos ≤ pat.size) (h₃ : needlePos ≤ stackPos)
      (h₄ : ∀ (j : ℕ) (hj : j < needlePos), pat[j] = s[stackPos - needlePos + j]) (h₅ : needlePos < pat.size)
      (h₆ : stackPos < s.size) (h₇ : pat[needlePos] = s[stackPos]), motive ⋯) →
    motive x