Derivazione del cubo (a) dal cubo (a) <-> a= a (Fitch)

Question

Sto cercando di dimostrare qualcosa in Fitch e sono bloccato su un passaggio, ho:

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

e voglio derivare 2. Cube(a) da questo.

So che è possibile perché posso utilizzare Ana Con su 2. e selezionare 1. come premessa e si dice che è valido.
C'è qualcuno che può dirmi come farlo senza utilizzare Ana Con?

Answer 1

(Non ho una copia di Fitch e non l'ho mai usata, quindi prendila con un pizzico di sale. Ma sono abbastanza sicuro che sia giusto.)

Per prima cosa ottieni solo "a= a" using= Intro.(Non hai bisogno di alcuna premessa.) Quindi prendi quello più il tuo 1. e applica <-> Elim per ottenere Cubo (a).