| _,None -> true
| Some t1',Some t2' -> aux context t1' t2'
) true l1 l2
- | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
+ | (C.Sort s1, C.Sort s2) when s1 = s2 || s2 = C.Type -> true
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
aux context s1 s2 &&
aux ((Some (name1, (C.Decl s1)))::context) t1 t2