On Sun, Jul 28, 2024 at 11:43 PM Glauco <[email protected]> wrote:
> I maybe wrong, but my feeling is that what Jagra calls A , in Mario's > translation is actually < A , 4 > (or < A, F(A) > , if you prefer). I meant it to be interpreted as <A, F(A)>, and part of the proof would be showing that F(A) = 4 so that the rest of the statement simplifies. (But that would seem to be part of the proof, not the formalization of the statement, if we want to read it literally.) -- 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/CAFXXJSuskqGnVR%3DJnqhrRR3ahd8V2JpgOSveNVrKBpr0Fxcb8w%40mail.gmail.com.
