start trying to prove RACONV_VSUBST

getting the statement right is going to be very difficult