我不喜欢看plt书的一大原因，就是证明太特么难看了，只有自然归纳或结构归纳这一种证明方法，证明主要是穷举结构归纳的case，还经常有两层的，核心技术是不要搞混了目标语言和元语言符号。我感觉Pierce开创用Coq教学plt的新局面，根本原因就是不上证明器就是在绕口令里徘徊。虽然教师这样讲课可能也没问题，学生作业收上来就吐血了，proof reading是体力活。

++++

妹想到序论和格论也没好到哪里去。不过话说回来，偏序和能归纳的结构还是很类似的，所以证明上接近也正常。好在序和格总归还是有点代数味道，结构归纳只有结论重要，证明的唯一目的是为了那个结论。