Totally agreed that we should be very cautious with these shortenings. We shared these dumps with the community because it would take us a lot of time to apply the level of care required to each of these theorems yet believe that they can also be useful as is.
We'll look into filtering the proofs that are safe to apply directly (no extra DVs and lowered or equivalent axiom trace), as this subset may be more useful to tackle first. -stan On Sat, Jul 4, 2020 at 8:50 PM Glauco <[email protected]> wrote: > > Additional distinct variable conditions can really weaken results (and / or > make theorems much more difficult to use) > > Glauco > > Il giorno sabato 4 luglio 2020 09:59:13 UTC+2, ookami ha scritto: >> >> Hmm. elsb4 has an extra distinct variable condition (x and y must be >> different), which the original theorem does not have. I did not look at the >> other results, but some care is in order, I think. >> >> Wolf >>> >>> > -- > 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/e2456dbb-8950-4d0f-85c1-98934557ee16o%40googlegroups.com. -- 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/CACZd_0xBqyPOgsaxAr%3Df%2BzPVZN7UYbnF3eSx7QZ5eg1y5s5NFw%40mail.gmail.com.
