Derivando o Cubo (a) do Cubo (a) <-> a= a (Fitch)

Question

Estou tentando provar algo no Fitch e estou preso em uma etapa, tenho:

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

e eu quero derivar 2. Cube(a) disso.

Sei que é possível porque posso usar Ana Con em 2. e selecionar 1. como premissa e ele diz que é válido.
Alguém pode me dizer como fazer isso sem usar Ana Con?

Answer 1

(Não tenho uma cópia do Fitch e nunca usei, então pegue isso com uma pitada de sal. Mas tenho certeza de que está certo.)

Primeiro, obtenha apenas "a= a" usando= Intro.(Você não precisa de nenhuma premissa.) Em seguida, pegue isso mais seu 1. e aplique <-> Elim para obter o Cubo (a).