Description: Specialization, using implicit substitution. Version of spim with a
disjoint variable condition, which does not require ax-13 . See
spimvw for a version with two disjoint variable conditions, requiring
fewer axioms, and spimv for another variant. (Contributed by NM, 10-Jan-1993)(Revised by BJ, 31-May-2019)