failed attempt to write alternate version of vsubst

wanted one with a slightly simpler definition that was equal to VSUBST.
failed because I tried to use finite maps, and VSUBST looks at shadowed
bindings in its association list. so I could make my "simpler" version
use an alist too, but then it's not really going to be much simpler.
Probably will make it simpler still (e.g. by unconditionally renaming to
a variant) and only try to prove ACONV results rather than equal..