`instantiate : instantiation -> term -> term`

SYNOPSIS
Apply a higher-order instantiation to a term.

DESCRIPTION
The call instantiate i t, where i is an instantiation as returned by term_match, will perform the instantiation indicated by i in the term t: types and terms will be instantiated and the beta-reductions that are part of higher-order matching will be applied.

FAILURE CONDITIONS
Should never fail on a valid instantiation.

EXAMPLE
We first compute an instantiation:
```  # let t = `(!x. P x) <=> ~(?x. P x)`;;
Warning: inventing type variables
val t : term = `(!x. P x) <=> ~(?x. P x)`

# let i = term_match [] (lhs t) `!p. prime(p) ==> p = 2 \/ ODD(p)`;;
val i : instantiation =
([(1, `P`)], [(`\p. prime p ==> p = 2 \/ ODD p`, `P`)],
[(`:num`, `:?61195`)])
```
and now apply it. Notice that the type variable name is not corrected, as is done inside PART_MATCH:
```  # instantiate i t;;
val it : term =
`(!x. prime x ==> x = 2 \/ ODD x) <=> ~(?x. prime x ==> x = 2 \/ ODD x)`
```

This is probably not useful for most users.