从多维数据集（a）导出多维数据集（a）<-> a= a（Fitch）

Question

我正在尝试在Fitch中证明某些东西，但我只能坚持一步，我有： 通用标签

并且我想从中得出2. Cube(a)。

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

Answer 1

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

首先使用= Intro获得“ a= a”。（您不需要任何前提。）然后将其加1.，然后应用<-> Elim来获取Cube（a）。