$`\newcommand{\Sep}{\mathrel{\|} } \newcommand{\Subst}[2]{ {\scriptsize \begin{bmatrix} #1\\ #2 \end{bmatrix} } } %`$$`\quad \alpha \Sep \varphi: \Gamma \to B`$ここで： 型コンテキストはギリシャ文字小文字 命題コンテキストはギリシャ大文字 命…