Получение куба (a) из куба (a) <-> a = a (Fitch)

Question

Я пытаюсь что-то доказать в Fitch, и я застрял на одном шаге, у меня есть:

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

и я хочу получить 2. Cube(a) От этого.

Я знаю, что это возможно, потому что я могу использовать Ana Con на 2. и выбрав 1. в качестве предпосылки, и он говорит, что это действительно.
Есть ли кто-нибудь, кто может сказать мне, как это сделать без использования Ana Con?

Answer 1

(У меня нет копии Fitch, и я никогда не использовал ее, поэтому возьмите это с щепоткой соли. Но я почти уверен, что это правильно.)

Сначала получите просто "a=a" используя =Intro. (Вам не нужны никакие помещения.) Затем возьмите это плюс ваш 1. и примените <->Elim, чтобы получить Cube(a).