+module NCicHash : Hashtbl.S with type key = NCic.term
+
+val mk_appl : NCic.term -> NCic.term list -> NCic.term
+
+(* the context is needed only to honour Barendregt's naming convention *)
+val apply_subst : NCic.substitution -> NCic.context -> NCic.term -> NCic.term
+val apply_subst_metasenv : NCic.substitution -> NCic.metasenv -> NCic.metasenv