Description: Move class substitution in and out of a function value, analogous to csbfv12 , with a direct proof proposed by Mario Carneiro, analogous to csbov123 . (Contributed by Alexander van der Vekens, 23-Jul-2017)