∀ {b e : String.Pos.Raw} (m : List Char)
  (motive : (∃ l m_1 r, Substring.Raw.ValidFor l m_1 r { str := String.ofList m, startPos := b, stopPos := e }) → Prop)
  (x : ∃ l m_1 r, Substring.Raw.ValidFor l m_1 r { str := String.ofList m, startPos := b, stopPos := e }),
  (∀ (ml mm mr : List Char)
      (h₂ : Substring.Raw.ValidFor ml mm mr { str := String.ofList m, startPos := b, stopPos := e }), motive ⋯) →
    motive x