For those who may be interested, the proposed shortenings have now been applied, along with an explanation of how I manually derived the one for L1 https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-11797219.
-- 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 visit https://groups.google.com/d/msgid/metamath/3d838cf6-f322-4344-8e6b-a241d710b501n%40googlegroups.com.
