1
4

1 回答 1

0

您的行的问题proof在于它proof旨在应用一些默认规则。在上面的证明中，Isabelle 无法弄清楚你想要进行存在性介绍。因此，您可能想明确告诉系统这样做，例如，通过继续使用类似proof (intro exI).

我希望这会有所帮助，勒内

于 2017-11-24T07:41:04.660 回答