inst : (hol_type * hol_type) list -> term -> term
# inst [`:num`,`:A`] `x:A = x`;; val it : term = `x = x` # type_of(rand it);; val it : hol_type = `:num`
# let tm = mk_abs(`x:A`,`x + 1`);; val tm : term = `\x. x + 1`
# inst [`:num`,`:A`] tm;; val it : term = `\x'. x + 1`