when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
C.Sort s2
| (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
+ | (C.Meta _, C.Sort _) -> t2'
+ | (C.Meta _, C.Meta (_,[]))
+ | (C.Sort _, C.Meta (_,[])) -> t2'
| (_,_) -> raise (TypeCheckerFailure (sprintf
"Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
(CicPp.ppterm t2')))