> > > Regarding your theorem ~elv: This can be applied only if sets (setvar > variables) are involved. Are there really so many proofs which can be > shortened using this theorem? > This could be checked by using the minimize script (checking all theorems > using ~vex). > > Actually, there are already 115 proofs (of theorems up to ~fnse in alphabetical order - I had to stop the minimize script here because the checks of the fourier* proofs take too long...) which can be shortened already now (without any other modifications in set.mm). Therefore, it could be a good idea to move this theorem to main set.mm, immediately following ~vex. What do others think about this?
-- 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/1dc55221-60b3-40dd-b6a6-b8e848d2131en%40googlegroups.com.
