val mk_appx : nf -> nf Listx.listx -> nf
val mk_match : nf i_num_var_ -> var -> int -> (int * nf) list ref -> nf list -> nf
val subst : bool -> bool -> int -> nf -> nf -> nf
val mk_appx : nf -> nf Listx.listx -> nf
val mk_match : nf i_num_var_ -> var -> int -> (int * nf) list ref -> nf list -> nf
val subst : bool -> bool -> int -> nf -> nf -> nf