Quick addendum: We already note that we allow several cases & still call it deduction form: http://us.metamath.org/mpeuni/mmnatded.html#special-cases
We could change the definition of "deduction form" to include them, & then note that in some cases you could use mainly deduction form with a few special cases. It makes the definition of "deduction form" longer, but it makes it much clearer what deduction form *is*. --- David A. Wheeler -- 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/ADC5426F-5D47-4B34-8515-26B383A4B8AF%40dwheeler.com.
