Note que, se $\downarrow p \not \leq [\![\varphi]\!]$, então $q' = \,\, \downarrow p - [\![\varphi]\!] \neq 0$.