Derivando el cubo (a) del cubo (a) <-> a= a (Fitch)

Question

Estoy tratando de probar algo en Fitch y estoy atascado en un paso, tengo:

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

y quiero derivar 2. Cube(a) de eso.

Sé que es posible porque puedo usar Ana Con en 2. y seleccionando 1. como premisa y dice que es válido.
¿Hay alguien que pueda decirme cómo hacer esto sin usar Ana Con?

Answer 1

(No tengo una copia de Fitch y nunca la he usado, así que tómate esto con una pizca de sal. Pero estoy bastante seguro de que es correcto).

Primero obtenga solo "a= a" usando= Intro.(No necesitas ninguna premisa). Luego toma eso más tu 1. y aplica <-> Elim para obtener Cube (a).