- open Rsyntax;
   open Rsyntax
   val INST = fn : term subst -> thm -> thm
   val INST_TYPE = fn : hol_type subst -> thm -> thm
   val INST_TY_TERM = fn : term subst * hol_type subst -> thm -> thm
   val SUBST = fn : {thm:thm, var:term} list -> term -> thm -> thm
   val SUBST_CONV = fn : {thm:thm, var:term} list -> term -> term -> thm
   val define_new_type_bijections = fn
     : {ABS:string, REP:string, name:string, tyax:thm} -> thm
   val dest_abs = fn : term -> {Body:term, Bvar:term}
   val dest_comb = fn : term -> {Rand:term, Rator:term}
   val dest_cond = fn : term -> {cond:term, larm:term, rarm:term}
   val dest_conj = fn : term -> {conj1:term, conj2:term}
   val dest_cons = fn : term -> {hd:term, tl:term}
   val dest_const = fn : term -> {Name:string, Ty:hol_type}
   val dest_disj = fn : term -> {disj1:term, disj2:term}
   val dest_eq = fn : term -> {lhs:term, rhs:term}
   val dest_exists = fn : term -> {Body:term, Bvar:term}
   val dest_forall = fn : term -> {Body:term, Bvar:term}
   val dest_imp = fn : term -> {ant:term, conseq:term}
   val dest_let = fn : term -> {arg:term, func:term}
   val dest_list = fn : term -> {els:term list, ty:hol_type}
   val dest_pabs = fn : term -> {body:term, varstruct:term}
   val dest_pair = fn : term -> {fst:term, snd:term}
   val dest_select = fn : term -> {Body:term, Bvar:term}
   val dest_type = fn : hol_type -> {Args:hol_type list, Tyop:string}
   val dest_var = fn : term -> {Name:string, Ty:hol_type}
   val inst = fn : hol_type subst -> term -> term
   val match_term = fn : term -> term -> term subst * hol_type subst
   val match_type = fn : hol_type -> hol_type -> hol_type subst
   val mk_abs = fn : {Body:term, Bvar:term} -> term
   val mk_comb = fn : {Rand:term, Rator:term} -> term
   val mk_cond = fn : {cond:term, larm:term, rarm:term} -> term
   val mk_conj = fn : {conj1:term, conj2:term} -> term
   val mk_cons = fn : {hd:term, tl:term} -> term
   val mk_const = fn : {Name:string, Ty:hol_type} -> term
   val mk_disj = fn : {disj1:term, disj2:term} -> term
   val mk_eq = fn : {lhs:term, rhs:term} -> term
   val mk_exists = fn : {Body:term, Bvar:term} -> term
   val mk_forall = fn : {Body:term, Bvar:term} -> term
   val mk_imp = fn : {ant:term, conseq:term} -> term
   val mk_let = fn : {arg:term, func:term} -> term
   val mk_list = fn : {els:term list, ty:hol_type} -> term
   val mk_pabs = fn : {body:term, varstruct:term} -> term
   val mk_pair = fn : {fst:term, snd:term} -> term
   val mk_primed_var = fn : {Name:string, Ty:hol_type} -> term
   val mk_select = fn : {Body:term, Bvar:term} -> term
   val mk_type = fn : {Args:hol_type list, Tyop:string} -> hol_type
   val mk_var = fn : {Name:string, Ty:hol_type} -> term
   val new_binder = fn : {Name:string, Ty:hol_type} -> unit
   val new_constant = fn : {Name:string, Ty:hol_type} -> unit
   val new_infix = fn : {Name:string, Prec:int, Ty:hol_type} -> unit
   val new_recursive_definition = fn
     : {def:term, fixity:fixity, name:string, rec_axiom:thm} -> thm
   val new_specification = fn
     : {consts:{const_name:string, fixity:fixity} list,
        name:string, sat_thm:thm}
       -> thm
   val new_type = fn : {Arity:int, Name:string} -> unit
   val new_type_definition = fn
     : {inhab_thm:thm, name:string, pred:term} -> thm
   val subst = fn : term subst -> term -> term
   val subst_occs = fn : int list list -> term subst -> term -> term
   val type_subst = fn : hol_type subst -> hol_type -> hol_type