The call vsubst [t1,x1; ...; tn,xn] t systematically replaces free instances
of each variable xi inside t with the corresponding ti from the
instantiation list. Bound variables will be renamed if necessary to avoid
capture.
FAILURE CONDITIONS
Fails if any of the pairs ti,xi in the instantiation list has xi and ti
with different types, or xi a non-variable. Multiple instances of the same
xi in the list are not trapped, but only the first one will be used
consistently.
EXAMPLE
Here is a relatively simple example
# vsubst [`1`,`x:num`; `2`,`y:num`] `x + y + 3`;;
val it : term = `1 + 2 + 3`
and here is a more complex instance where renaming of bound variables
is needed:
# vsubst [`y:num`,`x:num`] `!y. x + y < x + y + 1`;;
val it : term = `!y'. y + y' < y + y' + 1`
COMMENTS
An analogous function subst is more general, and will substitute for free
occurrences of any term, not just variables. However, vsubst is generally
much more efficient if you do just need substitution for variables.