几个例子表明，目标中的矛盾（例如当尝试对列表的长度使用归纳法时“0 > 0 意味着某些东西”）可以通过
exfalso. omega.
随着 Omega 模块被弃用，Omega 策略丢失了。处理上述情况的正确方法是什么？
谢谢你
不要使用
omega
lia
omega 策略已被弃用，取而代之的是 lia 策略。