1
4

1 回答 1

1

您的证明文本试图为两个不同的变量命名r。对于您的案例模式，请尝试使用不同的名称，例如case(TaTb l r'). 您将获得相同的证明状态，除了r'代替ra__.

于 2022-02-16T20:51:09.457 回答