> > How do I prove the last one in session 4: (A∨(A→⊥)→⊥)→⊥ ? >
Heh... That one looks daunting for some reason. But fear not, search for "Law of excluded middle implies double negation". Though, I was unable to find a solution until I solved it myself with much swearing and sweating :( -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c6908852-c9a6-4d73-97b5-9f4fa58e2434%40googlegroups.com.
