diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp
index 6d6b9be37..4efea6f37 100644
--- a/src/library/elaborator/elaborator.cpp
+++ b/src/library/elaborator/elaborator.cpp
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "kernel/builtin.h"
 #include "kernel/update_expr.h"
+#include "library/hidden_defs.h"
 #include "library/type_inferer.h"
 #include "library/elaborator/elaborator.h"
 #include "library/elaborator/elaborator_justification.h"
@@ -626,7 +627,7 @@ class elaborator::imp {
     int get_const_weight(expr const & a) {
         lean_assert(is_constant(a));
         optional<object> obj = m_env->find_object(const_name(a));
-        if (obj && obj->is_definition() && !obj->is_opaque())
+        if (obj && obj->is_definition() && !obj->is_opaque() && !is_hidden(m_env, const_name(a)))
             return obj->get_weight();
         else
             return -1;
diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp
index 1ddeb1913..28180f9fe 100644
--- a/src/library/hidden_defs.cpp
+++ b/src/library/hidden_defs.cpp
@@ -63,7 +63,7 @@ void set_hidden_flag(environment const & env, name const & d, bool flag) {
 
 void hide_builtin(environment const & env) {
     for (auto c : { mk_implies_fn(), mk_iff_fn(), mk_not_fn(), mk_or_fn(), mk_and_fn(),
-                mk_forall_fn(), mk_exists_fn(), mk_homo_eq_fn() })
+                mk_forall_fn() })
         set_hidden_flag(env, const_name(c));
 }
 
diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out
index e25f66c26..8226bf04c 100644
--- a/tests/lean/elab1.lean.expected.out
+++ b/tests/lean/elab1.lean.expected.out
@@ -130,47 +130,43 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
   Assumed: b
   Assumed: H
 Failed to solve
- ⊢ if ?M::0 (if (if ?M::3 (if a ⊥ ⊤) ⊤) ⊥ ⊤) ⊤ ≺ b
-    Normalize
-     ⊢ if ?M::0 (?M::3 ∧ a) ⊤ ≺ b
-        Substitution
-         ⊢ if ?M::0 ?M::1 ⊤ ≺ b
-            Normalize
-             ⊢ ?M::0 ⇒ ?M::1 ≺ b
-                (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
-            Assignment
-            H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1
-                Substitution
-                H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1
-                    Destruct/Decompose
-                     ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1
-                        (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of
-                            Discharge::explicit
+ ⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b
+    Substitution
+     ⊢ ?M::0 ⇒ ?M::1 ≺ b
+        (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
+        Assignment
+        H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1
+            Substitution
+            H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1
+                Destruct/Decompose
+                 ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1
+                    (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of
+                        Discharge::explicit
+                    with arguments:
+                        ?M::0
+                        ?M::1
+                        λ H1 : ?M::2, Conj H1 (Conjunct1 H)
+                Assignment
+                H1 : ?M::2 ⊢ a ≺ ?M::4
+                    Substitution
+                    H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4
+                        (line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of
+                            Conj::explicit
                         with arguments:
-                            ?M::0
-                            ?M::1
-                            λ H1 : ?M::2, Conj H1 (Conjunct1 H)
-                    Assignment
-                    H1 : ?M::2 ⊢ a ≺ ?M::4
-                        Substitution
-                        H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4
-                            (line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of
-                                Conj::explicit
-                            with arguments:
-                                ?M::3
-                                ?M::4
-                                H1
-                                Conjunct1 H
-                            Assignment
-                            H1 : ?M::2 ⊢ a ≈ ?M::5
-                                Destruct/Decompose
-                                H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6
-                                    (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of
-                                        Conjunct1::explicit
-                                    with arguments:
-                                        ?M::5
-                                        ?M::6
-                                        H
+                            ?M::3
+                            ?M::4
+                            H1
+                            Conjunct1 H
+                        Assignment
+                        H1 : ?M::2 ⊢ a ≈ ?M::5
+                            Destruct/Decompose
+                            H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6
+                                (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of
+                                    Conjunct1::explicit
+                                with arguments:
+                                    ?M::5
+                                    ?M::6
+                                    H
 Failed to solve
  ⊢ b ≈ a
     Substitution
@@ -342,50 +338,26 @@ Failed to solve
                  ⊢ ?M::1 ≈ Bool
                     Assumption 6
 Failed to solve
-a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ if (if a b ⊤) a ⊤ ≺ a
-    Normalize
-    a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
+a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
+    Substitution
+    a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1]
         Substitution
-        a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1]
-            Substitution
-            a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1]
-                Destruct/Decompose
-                a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1]
-                    (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
-                        DisjCases::explicit
-                    with arguments:
-                        ?M::3
-                        ?M::4
-                        ?M::5
-                        EM a
-                        λ H_a : ?M::6, H
-                        λ H_na : ?M::7, NotImp1 (MT H H_na)
-                 Normalize assignment
-                    ?M::0
-                    Assignment
-                    a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0
-                        Destruct/Decompose
-                        a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1]
-                            (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
-                                Discharge::explicit
-                            with arguments:
-                                ?M::0
-                                ?M::1
-                                λ H : ?M::2,
-                                  DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na))
-                    Assignment
-                    a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a
-                        Destruct/Decompose
-                        a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
-                            Destruct/Decompose
-                            a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
-                                Destruct/Decompose
-                                 ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
-                                    (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.
-            Assignment
-            a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ a
-                Substitution
-                a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ ?M::1[lift:0:1]
+        a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1]
+            Destruct/Decompose
+            a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1]
+                (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
+                    DisjCases::explicit
+                with arguments:
+                    ?M::3
+                    ?M::4
+                    ?M::5
+                    EM a
+                    λ H_a : ?M::6, H
+                    λ H_na : ?M::7, NotImp1 (MT H H_na)
+             Normalize assignment
+                ?M::0
+                Assignment
+                a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0
                     Destruct/Decompose
                     a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1]
                         (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
@@ -394,12 +366,33 @@ a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ if (if a b ⊤) a ⊤ ≺ a
                             ?M::0
                             ?M::1
                             λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na))
-                    Assignment
-                    a : Bool, b : Bool ⊢ ?M::1 ≈ a
+                Assignment
+                a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a
+                    Destruct/Decompose
+                    a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
                         Destruct/Decompose
-                        a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
+                        a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
                             Destruct/Decompose
-                            a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
-                                Destruct/Decompose
-                                 ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
-                                    (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.
+                             ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
+                                (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.
+        Assignment
+        a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ a
+            Substitution
+            a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ ?M::1[lift:0:1]
+                Destruct/Decompose
+                a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1]
+                    (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
+                        Discharge::explicit
+                    with arguments:
+                        ?M::0
+                        ?M::1
+                        λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na))
+                Assignment
+                a : Bool, b : Bool ⊢ ?M::1 ≈ a
+                    Destruct/Decompose
+                    a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
+                        Destruct/Decompose
+                        a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
+                            Destruct/Decompose
+                             ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
+                                (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.
diff --git a/tests/lean/elab6.lean b/tests/lean/elab6.lean
deleted file mode 100644
index be1ea8590..000000000
--- a/tests/lean/elab6.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
-        Abst (fun x, EqTIntro (H x))
diff --git a/tests/lean/exists4.lean.expected.out b/tests/lean/exists4.lean.expected.out
index 34137fd9b..d1b65d6aa 100644
--- a/tests/lean/exists4.lean.expected.out
+++ b/tests/lean/exists4.lean.expected.out
@@ -17,7 +17,7 @@ Theorem T1 : ∃ x y z : N, P x y z :=
         a
         (ExistsIntro::explicit
              N
-             (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)
+             (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)
              b
              (ExistsIntro::explicit N (λ z : N, P a b z) c H3))
 Theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
diff --git a/tests/lean/interactive/elab6.lean b/tests/lean/interactive/elab6.lean
new file mode 100644
index 000000000..9cf23fdbd
--- /dev/null
+++ b/tests/lean/interactive/elab6.lean
@@ -0,0 +1,9 @@
+(**
+-- The elaborator does not expand definitions marked as 'hidden'.
+-- To be able to prove the following theorem, we have to unmark the
+-- 'forall'
+local env = get_environment()
+set_hidden_flag(env, "forall", false)
+**)
+Theorem ForallIntro2 (A : (Type U)) (P : A -> Bool) (H : Pi x, P x) : forall x, P x :=
+        Abst (fun x, EqTIntro (H x))
diff --git a/tests/lean/elab6.lean.expected.out b/tests/lean/interactive/elab6.lean.expected.out
similarity index 67%
rename from tests/lean/elab6.lean.expected.out
rename to tests/lean/interactive/elab6.lean.expected.out
index 0049320f0..0ff7de0f8 100644
--- a/tests/lean/elab6.lean.expected.out
+++ b/tests/lean/interactive/elab6.lean.expected.out
@@ -1,3 +1,3 @@
-  Set: pp::colors
+#   Set: pp::colors
   Set: pp::unicode
   Proved: ForallIntro2
diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out
index a740b7192..618943f90 100644
--- a/tests/lean/tst6.lean.expected.out
+++ b/tests/lean/tst6.lean.expected.out
@@ -84,8 +84,8 @@ Theorem Example2 (a b c d : N)
                     a
                     b
                     c
-                    (Conjunct1::explicit (a == b) (b == c) H1)
-                    (Conjunct2::explicit (a == b) (b == c) H1))
+                    (Conjunct1::explicit (a == b) (eq::explicit N b c) H1)
+                    (Conjunct2::explicit (eq::explicit N a b) (b == c) H1))
                (Refl::explicit N b))
         (λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
            CongrH::explicit
@@ -98,8 +98,8 @@ Theorem Example2 (a b c d : N)
                     a
                     d
                     c
-                    (Conjunct1::explicit (a == d) (d == c) H1)
-                    (Conjunct2::explicit (a == d) (d == c) H1))
+                    (Conjunct1::explicit (a == d) (eq::explicit N d c) H1)
+                    (Conjunct2::explicit (eq::explicit N a d) (d == c) H1))
                (Refl::explicit N b))
   Proved: Example3
   Set: lean::pp::implicit