(* typecheck metasenv uri obj graph *)
(* refines [obj] and returns the refined form of [obj], *)
(* the new metasenv and universe graph. *)
(* the [uri] is required only for inductive definitions *)
val typecheck :
(* typecheck metasenv uri obj graph *)
(* refines [obj] and returns the refined form of [obj], *)
(* the new metasenv and universe graph. *)
(* the [uri] is required only for inductive definitions *)
val typecheck :