\def\nmodels{\not\nobreak\mkern -3mu \models}
\def\curlgdw{\prec\mkern -8mu \succ}
\newcommand{\ctl}[1]{\mbox{\textbf{#1}}}
