\textcolor{red}{TODO: metatheory documentation}