inst_goal : instantiation -> goal -> goal
Apply higher-order instantiation to a goal.
The call inst_goal i g where i is an instantiation (as returned by
term_match for example), will perform the instantiation indicated by i in
both assumptions and conclusion of the goal g.
- FAILURE CONDITIONS
Should never fail on a valid instantiation.
Probably only of specialist interest to those writing tactics from scratch.
- SEE ALSO
compose_insts, instantiate, INSTANTIATE, INSTANTIATE_ALL,