Case Study: Improving Reflection

我们在逻辑一章中看到，我们经常需要将布尔计算与Prop中的语句相关联。但是，在那里执行这种转换可能会导致冗长的验证脚本。考虑下面定理的证明：