computer-science - 从 Cube(a) <-> a = a (Fitch) 导出 Cube(a)

Question

我试图在 Fitch 中证明一些事情，但我被困在了一步，我有：

1.  Cube(a) <-> a = a

我想从中得到2. Cube(a)。

我知道这是可能的，因为我可以使用Ana Con2. 并选择 1. 作为前提，它说它是有效的。
有没有人可以告诉我如何在不使用的情况下做到这一点Ana Con？

Answer 1

（我没有 Fitch 的副本，也从未使用过它，所以请加一点盐。但我很确定它是正确的。）

首先使用 =Intro 得到“a=a”。（您不需要任何前提。）然后将其加上您的 1. 并应用 <->Elim 以获得 Cube(a)。