调整了一下定义，类比Curry的F和G组合子（和Π等价），如果逻辑弱到mltt的等式逻辑，则

F'αβM ≡ λx.= α x (B β M)
G'αβM ≡ λx.= α x (S (β x) M)

都可以把x抽象掉但是这样比较容易阅读。

++++

表面上看起来这是一个用于学习语言的简单解释器。但实际上稍微想一下就会发现，等词估值是在程序正式开始运行之前就可以静态估值的。而且所有等词一定能消去，如果有等词无法消去说明类型规则有问题。这样的话，类型检查和类型擦除都不需要写额外的算法，理论上。程序只要开始运行，运行到成为neutral的normal form。即可。

S (=α) (S (S(KB)(Kβ)) (KM))
S (=α) (S (S(KS) β ) (KM))