in
(* first we check if we are in the simple case of a meta closed term *)
let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =
in
(* first we check if we are in the simple case of a meta closed term *)
let subst,metasenv,ugraph1,hetype',he,args_bo_and_ty =