不久前我发了一篇关于等式理论的文章。文章中提到了，可以证明等式4蕴含等式7。虽然陶哲轩的博客上给出了一个证明，但是那个证明写得比较简短，略过了很多说明，所以看懂并不太容易。以下是我按照自己的理解改写的证明。
重新叙述问题如下：
公式4：
公式7：，此为交换律。
证明：公式4蕴含公式7。
这类问题的证明，可以看做一个字符串的“查找替换”过程，只需要遵守如下两条规则：
单个自由变量可以被替换为其他自由变量名或者其他自由变量的计算结果。比如y可以被替换成x，或者等等。
如果已经有，则所有的a可以被替换成b。
只要遵循以上两条规则，把一个公式替换成了另一个公式，则就完成了证明。以下是上述问题的证明过程。
开始，有式子1：
把替换为，得式子2:
在式子1中，把替换为，得式子3：
因为式子3，把式子2中的替换为，得式子4：
把式子1中的替换为，得式子5：
因为式子4，把式子5中的替换为，得式子6：
把式子6中的y替换为，得式子7，其本质上是说和之间符合交换律:
把式子1中的y替换为，得式子8：
把式子1中的替换为，替换为，得式子：
因为式子9，把式子8中的替换成，得：
上式实际上已经证明式子7的左边是。
接下来把把式子1中的替换为，替换为，得式子：
因为式子1，把式子10中的替换为，等式子11：
上式实际上已经证明式子7的右边是。
所以，根据等式7，我们得到了
证毕，是不是繁复无比！
想必此时你已经在考虑，是否可以通过写一个电脑程序，通过不断地查找替换，来判定两个式子之间是否有蕴含关系。但此类问题已经被证明是不可判定的(undecideable)，也就是不可能存在这样的电脑程序，可以在有限时间内，确定性的完成判定。
因为这种不可决定性，以及证明的繁复，所以这类问题特别适合Lean Prover，因为Lean可以确保证明结论的正确性。
