Description: Obsolete as of 30-Jul-2023. Use sb4b instead. One direction of a
simplified definition of substitution when variables are distinct.
(Contributed by NM, 14-May-1993) Revise df-sb . (Revised by Wolf
Lammen, 25-Jul-2023)(Proof modification is discouraged.)(New usage is discouraged.)