اشتقاق المكعب (أ) من المكعب (أ) <-> a = a (فيتش)

Question

أحاول إثبات شيء ما في وكالة فيتش وأنا عالق في خطوة واحدة، لدي:

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

وأريد أن أستنتج 2. Cube(a) من ذاك.

أعلم أنه ممكن لأنني أستطيع استخدامه Ana Con على 2.واختيار 1.كمقدمة وتقول أنها صالحة.
هل هناك أي شخص يمكن أن يقول لي كيفية القيام بذلك دون استخدام Ana Con?

Answer 1

(ليس لدي نسخة من فيتش ولم أستخدمها مطلقًا، لذا تعامل مع هذا مع قليل من الملح.لكنني متأكد من أنه على حق.)

احصل أولاً على "a=a" باستخدام =Intro.(لا تحتاج إلى أي مقر.) ثم خذ هذا بالإضافة إلى 1.وقم بتطبيق <->Elim للحصول على Cube(a).