> I guess there's the concept of "definition" for those terms(?) : can it be > rendered in a linked html page? >
Browsing this page https://digama0.github.io/mm0/peano/index.html I may be wrong, but it looks like "nat" and "+" in Peano are not eliminable, kind of "e." is not eliminable in ZF , so my question is probably ill-posed -- 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/6a622530-e403-43d0-962d-8526bd54e1e8n%40googlegroups.com.
