\[
\definecolor{leff}{RGB}{255,107,102}
\definecolor{lcoeff}{RGB}{102,63,180}
\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{\?}{?}
\newcommand{\highlight}[1]{\bbox[yellow]{#1}}
\newcommand{\Int}{\mathsf{Int}}
\newcommand{\Boolean}{\mathsf{Bool}}
\newcommand{\Bool}{\mathsf{Bool}}
\newcommand{\Unit}{\mathsf{Unit}}
\newcommand{\?}{\mathsf{?}}
\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{\fst}{{\mathsf{fst}}}
\newcommand{\snd}{{\mathsf{snd}}}
\newcommand{\prot}[6]{{\mathsf{prot}^{{#5,#2,#3}}_{#6,#1} #4}}
\newcommand{\ite}[3]{\mathsf{if} ~#1~ \mathsf{then} ~#2 ~\mathsf{else}~ #3}
\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{\gsum}{\oplus}
\newcommand{\evidence}[1]{\style{font-size:80%;opacity: 0.8}{\color{lcoeff} \langle#1\rangle}~}
\newcommand{\evidencee}[1]{\style{font-size:80%;opacity: 0.8}{\color{lcoeff} \langle#1\rangle}~}
\newcommand{\evidencees}[2]{\style{font-size:80%;opacity: 0.8}{\color{lcoeff} \langle#1\rangle^{#2}}~}
\newcommand{\evidenceeu}[2]{\style{font-size:80%;opacity: 0.8}{\color{lcoeff} {}^{#2}\langle#1\rangle}~}
\newcommand{\evidenceesu}[3]{\style{font-size:80%;opacity: 0.8}{\color{lcoeff} {}^{#3}\langle#1\rangle^{#2}}~}
\newcommand{\pack}[4]{\mathsf{pack}(#1, #2)~\mathsf{as}~\exists #3.#4}
\newcommand{\npack}[4]{\mathsf{unpack}(#1, #2) = #3~\mathsf{in}~#4}
\newcommand{\sub}{<:}
\newcommand{\csub}{\widetilde{\sub}}
\newcommand{\subl}{\preccurlyeq}
\newcommand{\csubl}{\widetilde{\subl}}
\newcommand{\vunit}{\mathsf{unit}}
\]