The proof of nnne0ALT is a thin wrapper of 0nnn, which is in turn a thin wrapper of nnne0, which makes me think why this alternative proof is kept. The caption says that it is supposed to be a shorter proof using more axioms, but it seems not the case, at least for the current version of set.mm.
-- 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/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com.
