∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.ForwardPatternModel pat] {s : String.Slice} {pos : s.Pos}
  (motive :
    (∃ endPos, ∃ (h : pos ≤ endPos), String.Slice.Pattern.Model.IsLongestMatch pat (pos.sliceFrom endPos h)) → Prop)
  (x : ∃ endPos, ∃ (h : pos ≤ endPos), String.Slice.Pattern.Model.IsLongestMatch pat (pos.sliceFrom endPos h)),
  (∀ (p : s.Pos) (h₁ : pos ≤ p) (h₂ : String.Slice.Pattern.Model.IsLongestMatch pat (pos.sliceFrom p h₁)), motive ⋯) →
    motive x