idea for raconv_vsubst that unfortunately doesn't work

wanted to compute the term with the bound variables renamed but without
the substitution first, and prove that it was alpha-equivalent to the
original but could be simply substituted through. but the first
condition may be false: the new name that VSUBST chooses for the bound
variable might only be safe after the whole substitution is applied.