> > Very interesting. Arguably higher level theorems proofs would > eventually become ~~ similar?
I think so. For example, compare rpneg <http://us2.metamath.org:88/mpeuni/rpneg.html> from set.mm and rpnegap <http://us2.metamath.org:88/ileuni/rpnegap.html> from iset.mm - they are certainly similar but not the same (maybe Jim could comment on how well proofs of high-level theorems translate from set.mm to iset.mm). -- 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/aed41439-97b7-48c9-aba0-3fbbfa1a942e%40googlegroups.com.
