| _ -> [],newmeta,[],term
in
let metasenv' = metasenv@newmetasenvfragment in
-prerr_endline ("^^^^^TERM': " ^ CicPp.ppterm term') ;
let termty =
CicSubstitution.subst_vars exp_named_subst_diff
(CicTypeChecker.type_of_aux' metasenv' context term)
in
-prerr_endline ("^^^^^TERMTY: " ^ CicPp.ppterm termty) ;
(* newmeta is the lowest index of the new metas introduced *)
let (consthead,newmetas,arguments,_) =
new_metasenv_for_apply newmeta' proof context termty