小编lam*_*bda的帖子

当在coqide中构建证明时，我没有找到方法

T1; T2; T3; ...; Tn.

一种策略一种策略。因此，像上面的代码那样构造正确的证明变得非常困难。所以我的问题是

• 有没有办法逐步浏览上面的代码，或者
• 您如何像上面的代码那样构造证明？

转发一个命令或转到光标均无效。