On Fri, 10 Apr 2020 03:33:42 -0700 (PDT), Thomas Brendan Leahy <[email protected]> wrote: > I've deleted the proof itself, but to give you an idea, here's an HTML file > I made.
Unless you object, I'm going to retype that proof aacllem from the HTML, submit it to set.mm, and give you credit. That looks like something potentially useful, it's a lot of work to get that (440 steps!), and you posted it here as HTML so I'm assuming you intended for it to get into set.mm. Please let me know if you object! --- David A. Wheeler -- 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/E1jSCro-0004b7-TR%40rmmprod06.runbox.
