Given two instantiations i1 and i2 (with type instantiation, as returned
by term_match for example), the call compose_insts i1 i2 will give a new
instantiation that results from composing them, with i1 applied first and
then i2. For example, instantiate (compose_insts i1 i2) t should be the
same as instantiate i2 (instantiate i1 t).
FAILURE CONDITIONS
Never fails.
COMMENTS
Mostly of specialized interest; used in sequencing tactics like THEN to
compose metavariable instantiations.