diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index b8c1f7743..3a72115e8 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -68,7 +68,7 @@ theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) :
 theorem not_intro {a : Bool} (H : a → false) : ¬ a
 := H
 
-theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
+theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
 := funext (λ x : A, refl (f x))
 
 theorem trivial : true
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 09bb74a84..15c4f9d2e 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp
index 3ed96a374..75dfd8f7c 100644
--- a/src/library/simplifier/ceq.cpp
+++ b/src/library/simplifier/ceq.cpp
@@ -115,33 +115,42 @@ list<expr_pair> to_ceqs(ro_environment const & env, expr const & e, expr const &
 }
 
 bool is_ceq(ro_environment const & env, expr e) {
-    buffer<bool> in_lhs;
+    buffer<bool> found_args;
+    // Define a procedure for marking arguments found.
+    auto visitor_fn = [&](expr const & e, unsigned offset) {
+        if (is_var(e)) {
+            unsigned vidx = var_idx(e);
+            if (vidx >= offset) {
+                vidx -= offset;
+                if (vidx >= found_args.size()) {
+                    // it is a free variable
+                } else {
+                    found_args[found_args.size() - vidx - 1] = true;
+                }
+            }
+        }
+        return true;
+    };
+
     context ctx;
     while (is_pi(e)) {
+        if (!found_args.empty()) {
+            // Support for dependent types.
+            // We may find the instantiation for the previous variables
+            // by matching the type.
+            for_each(abst_domain(e), visitor_fn);
+        }
         // If a variable is a proposition, than if doesn't need to occurr in the lhs.
         // So, we mark it as true.
-        in_lhs.push_back(env->is_proposition(abst_domain(e), ctx));
+        found_args.push_back(env->is_proposition(abst_domain(e), ctx));
         ctx = extend(ctx, abst_name(e), abst_domain(e));
         e = abst_body(e);
     }
     if (is_eq(e)) {
         expr lhs = arg(e, 2);
         // traverse lhs, and mark all variables that occur there in is_lhs.
-        for_each(lhs, [&](expr const & e, unsigned offset) {
-                if (is_var(e)) {
-                    unsigned vidx = var_idx(e);
-                    if (vidx >= offset) {
-                        vidx -= offset;
-                        if (vidx >= in_lhs.size()) {
-                            // it is a free variable
-                        } else {
-                            in_lhs[in_lhs.size() - vidx - 1] = true;
-                        }
-                    }
-                }
-                return true;
-            });
-        return std::find(in_lhs.begin(), in_lhs.end(), false) == in_lhs.end();
+        for_each(lhs, visitor_fn);
+        return std::find(found_args.begin(), found_args.end(), false) == found_args.end();
     } else {
         return false;
     }
diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua
index 3f9255959..dcedf3ca6 100644
--- a/tests/lua/ceq1.lua
+++ b/tests/lua/ceq1.lua
@@ -34,7 +34,7 @@ test_ceq("Ax3", 4)
 test_ceq("Ax4", 0)
 test_ceq("Ax5", 1)
 test_ceq("Ax6", 1)
--- test_ceq("eta", 1)
+test_ceq("eta", 1)
 test_ceq("not_not_eq", 1)
 test_ceq("or_comm", 1)
 test_ceq("or_assoc", 1)