@AndreasBlass I don't think it is wrong and I also think that it should be that. But the problem for me is that there is only defined $D_\infty \vDash M=N \iff \llbracket M\rrbracket_\rho = \llbracket N\rrbracket_\rho$. En we can indeed as you suggest then write $D_\infty \vDash M\sqsubseteq N \iff \llbracket M\rrbracket_\rho \sqsubseteq \llbracket N\rrbracket_\rho$. But since it isn't defined I'm not sure about it.