在 一步规约 与 类型与类型判断 的规则里， ${𝑡}_1,{𝑡}_2,{𝑡}_1^{\prime }$ 等字母是元变量： 它们属于元语言，可以代换为 词项的集合 中的任意词项； 对象语言自身没有变量． $𝑣$ 只能代换为值， nv 只能代换为数值 （ 值与数值 ）， $𝑇$ 则只能代换为类型． 同一条规则中同一个元变量的所有出现必须使用相同的代换． 因此，一条推导规则概括了许多具体实例．