柯里－霍华德对应

类型对应命题，程序对应证明。写一个类型正确的程序，就是给出了一个证明。