| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
aux true context s1 s2 &&
aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
aux true context s1 s2 &&
aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2