if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
assert false ; (* not possible, error in CicUniv *)
C.Sort (C.Type t'),subst,metasenv
if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
assert false ; (* not possible, error in CicUniv *)
C.Sort (C.Type t'),subst,metasenv