Type.type

If theta = [{redex_1,residue_1},...,{redex_n,residue_n}] is a (hol_type,hol_type) subst, where the redex_i are the types to be substituted for, and the residue_i the replacements, and ty is a type to instantiate, the call type_subst theta ty will replace each occurrence of a redex_i by the corresponding residue_i throughout ty. The replacements will be performed in parallel. If several of the type instantiations are applicable, the choice is undefined. Each redex_i ought to be a type variable, but if it isn’t, it will never be replaced in ty. Also, it is not necessary that any or all of the types redex_1...redex_n should in fact appear in ty.