(fun b t1 t2 ->
b &&
match t1,t2 with
- None,None -> true
+ None,_
+ | _,None -> true
| Some t1',Some t2' -> aux context t1' t2'
- | _,_ -> false
) true l1 l2
| (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->