(* type_of_aux' metasenv context term *)
(* refines [term] and returns the refined form of [term], *)
(* its type, the computed substitution and the new metasenv. *)
(* type_of_aux' metasenv context term *)
(* refines [term] and returns the refined form of [term], *)
(* its type, the computed substitution and the new metasenv. *)