Improve discussion text explaining ex-natded5.13
Improve discussion text explaining ex-natded5.13

This adds a cross-reference from each original step# to the
corresponding step# in the MPE proof, along with with some other
improvements, to ex-natded5.13.  The intent is to make it easier
to understand how to do natural deduction in MPE by proving some
worked examples.

metamath/set.mm,metamath/set.mm,metamath/set.mm