| Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
| _ :: tail -> aux (succ p) tail
| Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp ->
p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph)
| _ :: tail -> aux (succ p) tail