refactor(builtin/kernel): mark exists as opaque after proving key theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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).
+              (assume H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), UnfoldExists2 a H).
+
+SetOpaque exists true.

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,

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))