\[
\definecolor{leff}{RGB}{255,107,102}
\definecolor{lcoeff}{RGB}{78,206,88}
\definecolor{ltyp}{RGB}{255,202,79}
\definecolor{lkvd}{RGB}{127,165,255}
\definecolor{eff}{RGB}{177,35,43}
\definecolor{coeff}{RGB}{35,177,53}
\definecolor{typ}{RGB}{177,93,43}
\definecolor{expr}{RGB}{0,0,0}
\definecolor{kvd}{RGB}{0,45,177}
\definecolor{num}{RGB}{43,177,93}
\newcommand{\highlightType}[1]{{\color{typ} #1}}
\newcommand{\highlight}[1]{\bbox[yellow]{#1}}
\newcommand{\bboxStart}{{\color{red}{\big[}}}
\newcommand{\bboxEnd}{{\color{red}{\big]}}}
\newcommand{\Int}{\mathsf{Int}}
\newcommand{\Boolean}{\mathsf{Bool}}
\newcommand{\Unit}{\mathsf{Unit}}
\newcommand{\Ref}[1]{\mathsf{Ref}~#1}
\newcommand{\Refl}[2]{\mathsf{Ref}_{#1}~#2}
\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}
\newcommand{\reff}{{\mathsf{ref}~}}
\newcommand{\protold}[6]{{\mathsf{prot}^{{#5,#2,#3}}_{#6,#1} #4}}
\newcommand{\prot}[7]{{\mathsf{prot}^{{#5,#2,#3}}_{#1} #6#7~ (#4)}}
\newcommand{\protList}[6]{{\mathsf{prot}^{{#4,#2,#3}}_{#1} #5#6~}}
\newcommand{\ite}[3]{\mathsf{if} ~#1~ \mathsf{then} ~#2 ~\mathsf{else}~ #3}
\newcommand{\itei}{\mathsf{if}~}
\newcommand{\itet}{\mathsf{then}~}
\newcommand{\itee}{\mathsf{else}~}
\newcommand{\TermTold}[1]{{\color{kvd} \oblset{Term}_{#1}}}
\newcommand{\TermT}[1]{{\color{kvd} {#1}}}
\newcommand{\oblset}[1]{\textsf{#1}}
\newcommand{\ljoin}{\style{display: inline-block; margin-top:3px; transform:rotate(-0.25turn);}{\prec}}
\newcommand{\lmeet}{\style{display: inline-block; transform:rotate(0.25turn);}{\prec}}
\newcommand{\cjoin}{\widetilde{\ljoin}}
\newcommand{\cmeet}{\widetilde{\lmeet}}
\newcommand{\sub}{<:}
\newcommand{\csub}{\widetilde{\sub}}
\newcommand{\subl}{\preccurlyeq}
\newcommand{\csubl}{\widetilde{\subl}}
\newcommand{\vunit}{\mathsf{unit}}
\]