判断シーケント＝関数定義があるとする。
$`\quad a : (\Gamma \vdash t : \beta)`$
これを次のようにパックする。
$`\quad (a : [\Gamma \to \beta], a := t^\wedge)`$
ここで、$`t^\wedge`$ は項のフルカリー化。パックした定義は、環境コンテキストに追加できて、追加した後の環境コンテキスト（混合コンテキスト）も正当〈correct〉になる。
判断シーケント＝関数定義があるとする。
$`\quad a : (\Gamma \vdash t : \beta)`$
これを次のようにパックする。
$`\quad (a : [\Gamma \to \beta], a := t^\wedge)`$
ここで、$`t^\wedge`$ は項のフルカリー化。パックした定義は、環境コンテキストに追加できて、追加した後の環境コンテキスト（混合コンテキスト）も正当〈correct〉になる。