NCic.metasenv * NCic.substitution
(* this should be moved elsewhere *)
-val fix_sorts: NCic.term -> NCic.term
+val fix_sorts:
+ NCic.metasenv -> NCic.substitution ->
+ NCic.term -> NCic.metasenv * NCic.term
(* delift_type_wrt_terms st m s c t args
* lift t (length args)