从低阶类型到高阶类型

参考资料：Type Theory and Formal Proof