It sounds like we were unable to prevent a proof modification in this case. We'll have to go back through the history to find out what the original proof was and how it degenerated.
On Wed, Feb 1, 2023 at 12:54 PM Zheng Fan <fanzheng1...@outlook.com> wrote: > 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 metamath+unsubscr...@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/65b3f52c-17c8-42c5-8349-582f2ff86bd8n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSu_SWsfjpFEhshPaNYC4LahujxLBP-%3DU%3Du5PMwCxjdzSg%40mail.gmail.com.
