推理规则：
- 全称、存在的特指规则 US ES
- 全称、存在的推广规则 UG EG
一般放在前面，后面接上引用的行数
指派：
- 全称量词可以指派任意变量，和一个特定的变量
- 存在量词可以指派一个特定的变量
在结论里面的全称命题，都换成 Skolem变量（）
结论里面的存在命题，可以先用一个变量代着
越靠近命题越强
注意 S/G 规则使用的时候
指派变量的时候注意对象是严格的同一个对象，即换名字换的是同一个人，而且换了之后不能重名
Warning
在使用 ES 规则的时候，如果在辖域内有其他自由变元存在，那么指派的应该是在辖域内其他自由变元的函数