computer-science - Cube（a）からCube（a）を導出する<-> a = a（フィッチ）

Question

私はフィッチで何かを証明しようとしています、そして私は一歩で立ち往生しています、私は持っています：

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

そして私はそれから導き出したいです2. Cube(a)。

私はAna Con2.で使用でき、前提として1.を選択できるので、それが可能であることを知っています。それは有効であると言っています。
使用せずにこれを行う方法を教えてくれる人はいますAna Conか？

Answer 1

(私は Fitch のコピーを持っておらず、一度も使用したことがないので、これを少しの塩と考えてください。しかし、私はそれが正しいと確信しています。)

最初に =Intro を使用して "a=a" だけを取得します。(前提は必要ありません。) 次に、それに 1 を足して、<->Elim を適用して Cube(a) を取得します。