做了一个违背祖宗的决定，把Ξ，F，G组合子都抛弃了，直接把⊢写在公式里。

Mα⊢β，这是函数M的类似是α⊢β的意思，elim的推导过程比较狂野。

Mα⊢β
⊢β(Mα)
⊢BβMα
α⊢BβM，此时可以加入公式N⊢α，应用cut
N⊢BβM
⊢BβMN
⊢β(MN)

Mα⊢βα，这是依赖函数，但是和Martin Lof版本的不一样因为这里有两个α，都是要拿去cut的，换句话说这是线性版本。

Mα⊢βα
⊢βα(Mα)
⊢Cβ(Mα)α，不唯一，可以先消另一个α
α⊢Cβ(Mα)
N⊢Cβ(Mα)，cut第一个α
⊢Cβ(Mα)N
⊢βN(Mα)
⊢B(βN)Mα，
⊢B(βN)MN，cut第二个α
⊢βN(MN)

------------

我还没搞明白为什么这种演算方式是work的，一个可能性是因为这里只有蕴含的引入和消去，λ的带入被合并在一起co deduction了，但其中左右移动项或类型还是有点奇怪，它「象」，但不完全是，演绎定理中可以把蕴含来回搬的情况，以及蕴含的左右引入。

这个演算的一大特色是如果把项和类型统一成一个字母表，其实看不出哪个是项哪个是类型了。而依赖类型是线性规则，至少是无收缩的，因此没有宇宙也不该有悖论产生。