在 [定义] 一步归约 与 [定义] 类型与类型判断 的规则里，${𝑡}_1,{𝑡}_2,{𝑡}_{1^{\prime }}$ 等字母是元变量（metavariable）：它们是元语言里的变量，可以代换成 [定义] 项的集合 中的任意项； 只能代换成 [定义] 值与数值 中的数值。同一条规则里同一个字母必须代换成同一个东西。一条规则因此代表无穷多条实例（instance）。