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/a55d60ef-3516-4f51-af02-ea5f3730a685%40googlegroups.com.
