diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index ca95b1bb8..903ecea16 100644
--- a/src/builtin/kernel.lean
+++ b/src/builtin/kernel.lean
@@ -361,4 +361,6 @@ Theorem UnfoldExists2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x :
 
 Theorem UnfoldExists {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x))
 := ImpAntisym (assume H : (∃ x : A, P x), UnfoldExists1 a H)
-              (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H).
\ No newline at end of file
+              (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H).
+
+SetOpaque exists true.
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 41d411e44..cbad4b0e0 100644
Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ
diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean
index 6c68ab015..50c4cbd52 100644
--- a/tests/lean/exists3.lean
+++ b/tests/lean/exists3.lean
@@ -1,6 +1,8 @@
 Import int.
 Variable P : Int -> Int -> Bool
 
+SetOpaque exists false.
+
 Theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) :=
          ForallIntro (fun a,
              ForallIntro (fun b,
diff --git a/tests/lean/exists4.lean.expected.out b/tests/lean/exists4.lean.expected.out
index b75fda078..582b65c90 100644
--- a/tests/lean/exists4.lean.expected.out
+++ b/tests/lean/exists4.lean.expected.out
@@ -15,7 +15,7 @@ Theorem T1 : ∃ x y z : N, P x y z :=
         N
         (λ x : N, ∃ y z : N, P x y z)
         a
-        (@ExistsIntro N (λ x : N, ¬ (∀ x::1 : N, ¬ P a x x::1)) b (@ExistsIntro N (λ z : N, P a b z) c H3))
+        (@ExistsIntro N (λ y : N, ∃ z : N, P a y z) b (@ExistsIntro 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))
 Theorem T3 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
 Theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro a (ExistsIntro b H))