導出キューブ（a）は（a）の<-> =（フィッチ）

Question

私はフィッチで何かを証明しようとしていると私は一歩にこだわって、私が持っている：

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

と私それから2. Cube(a)を派生させたい。

私はAna Conを2.に使い、1.を前提として選択しているので、それは可能です。
Ana Conを使用せずにこれを行う方法を教えてもらえますか？

Answer 1

（私はフィッチのコピーを持っていないし、それを使ったことがないので、塩のピンチでこれを取る。しかし、私はそれが正しいだと確信しています。）

まず単に「A = Aを取得します"using = Intro。 （あなたは何も前提は必要ありません。）そしてそれにあなたの1.を加え、< - > Elimを適用してCube（a）を入手してください。