(* 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
(* 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