List.fold_right
(fun (name, _, typ, _) (metasenv, types) ->
let new_metasenv, new_type = aux metasenv context typ in
-prerr_endline ("UH? " ^ CicPp.ppterm typ ^ " ==> " ^ CicPp.ppterm new_type) ;
(new_metasenv, (name, new_type) :: types))
funs (metasenv, [])
in