Description: A representation of explicit substitution of a class for a variable, inferred from an implicit substitution hypothesis. (Contributed by NM, 18-Aug-1993) Avoid ax-12 . (Revised by SN, 8-Sep-2024)