- | (C.Prod (_,s1,t1), C.Prod(_,s2,t2)) ->
- aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2
- | (C.Lambda (_,s1,t1), C.Lambda(_,s2,t2)) ->
- aux context s1 s2 && aux ((C.Decl s1)::context) t1 t2
- | (C.LetIn (_,s1,t1), C.LetIn(_,s2,t2)) ->
- aux context s1 s2 && aux ((C.Def s1)::context) t1 t2
+ | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+ aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+ | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
+ aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+ | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
+ aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2