try
let _,c,_,ty = U.lookup_subst n subst in c,ty
with U.Subst_not_found _ -> try
let _,_,c,ty = U.lookup_meta n metasenv in c,ty
with U.Meta_not_found _ ->
raise (AssertFailure (lazy (Printf.sprintf
try
let _,c,_,ty = U.lookup_subst n subst in c,ty
with U.Subst_not_found _ -> try
let _,_,c,ty = U.lookup_meta n metasenv in c,ty
with U.Meta_not_found _ ->
raise (AssertFailure (lazy (Printf.sprintf