Extend documentation on deduction
Extend documentation on deduction

Extend documentation on deduction using recent text posted on the
mailing list.  (Almost all of this text is originally from Normal Megill;
I've tweaked it so it hopefully flows in context.)

Signed-off-by: David A. Wheeler <9ae72d22d8b894b865a7a496af4fab6320e6abb2@dwheeler.com>

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