Description: A composition law for substitution. Version of sbco with a disjoint variable condition using fewer axioms. (Contributed by NM, 14-May-1993) (Revised by GG, 7-Aug-2023)