The definable $(p,q)$-theorem for distal theories

Let $M\prec N$ be NIP $L$-structures. Let $\varphi(x,y)$ be an $L_M$-formula and let $b\in N^{|y|}$. Assume $\varphi(x,b)$ does not divide over $M$. Chernikov–Simon conjecture. There is an $L_M$-formula $\psi(y)\in\operatorname{tp}(b/M)$ such that

$$\{\varphi(x,b^\prime):b^\prime\in\psi(M)\}\text{ is consistent}.$$

This is a definable analogue of the combinatorial $(p,q)$-theorem and was posed by Chernikov and Simon as a question before becoming a conjecture. The paper answers this special case affirmatively for distal NIP theories, so the conjecture is solved in the stated setting.