See my note here: https://github.com/metamath/set.mm/pull/1292#issuecomment-561838231
Norm On Saturday, December 7, 2019 at 8:52:14 AM UTC-5, fl wrote: > > I do not want to be ironic, of course, but I have the impression that we > first replaced the > venerable"( ph -> A. x ph)" by" F/ x ph" supposed to be more meaningful > and that now > to put in common factor some parts of the proofs we reintroduce"( ph -> A. > x ph)" > beside" F/ x ph" finally returning to the previous state and multiplying > the proofs by two. > > And we hope to fight against ecological disaster. > > This civilization will die crushed under its own weight. > > (By the way "Google Translate" may I recall Thee that the translation of > the > French word "démonstration" is "proof" not "demonstration". Please !) > > -- > FL > -- 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/b376da0b-51ac-4b28-916f-26f093aa0d94%40googlegroups.com.
