我要学数学—G系统的∀R

在数理逻辑的学习过程中，对自然推理系统G中的VR规则总是难以理解，在G系统的soundness证明时也用“同理可证”一笔带过，现在遇到了下述问题：

这里对新变元的概念做出了澄清，可见当∀落在后件中时，只能被替换一次，并且不能与之前的替换重复。