Description: Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019)