I'm afraid that your x_ne_y axiom is already too "powerful" and "extending" the example is not gonna help (if you mean "adding" statements)
You might replace x_ne_y with something like 0_ne_1 $a true 0 != 1 $. 1_ne_0 $a true 1 != 0 $. but, of course, this does not scale at all Glauco -- 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/f6116ed2-6440-4a22-be6b-9a9061cb032dn%40googlegroups.com.
