Description: Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019) (Proof shortened by Wolf Lammen, 31-May-2025)