diff --git a/prelude/core/boolean_props.lp b/prelude/core/boolean_props.lp
index aca40ad983be075a031d70a776336e18883a1e58..ef0422d971057775dde7b522dc9f1443ce9e33f6 100644
--- a/prelude/core/boolean_props.lp
+++ b/prelude/core/boolean_props.lp
@@ -1,13 +1,6 @@
 require open encodings.pvs_core
 prelude.core.booleans prelude.core.equalities prelude.core.if_def
 
-// true /= false
-symbol bool_inclusive : eps (bnot (eq bool false true))
-
-// A ∨ ¬ A
-symbol bool_exclusive (A:eta bool):
-    eps (bor (eq bool A false) (eq bool A true))
-
 theorem excluded_middle : ∀ A : eta bool, eps (bor A (bnot A))
 proof
 admit
diff --git a/prelude/core/if_def.lp b/prelude/core/if_def.lp
index ede0300ca27cb9c1ee51748f932eb3b54ac0a043..6e4868bebcdbb119e3b13cb8d76c36e877e8b479 100644
--- a/prelude/core/if_def.lp
+++ b/prelude/core/if_def.lp
@@ -1,4 +1,4 @@
 require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
 prelude.core.notequal
 
-symbol if (T:Type): eta bool ⇒ eta T ⇒ eta T ⇒ eta T
+symbol if {T:Type}: η bool ⇒ eta T ⇒ eta T ⇒ eta T
diff --git a/prelude/core/pvs_core.lp b/prelude/core/pvs_core.lp
deleted file mode 120000
index bd5d0b0e2db6e9deb375ff1d5f94dbfd5c25f284..0000000000000000000000000000000000000000
--- a/prelude/core/pvs_core.lp
+++ /dev/null
@@ -1 +0,0 @@
-../pvs_core.lp
\ No newline at end of file
diff --git a/prelude/core/quantifier_props.lp b/prelude/core/quantifier_props.lp
index 85c51a98053768f539a2b94dc84866624e1436cb..b803f5fc4b3931039a9a8d0e45a41c3d899c0370 100644
--- a/prelude/core/quantifier_props.lp
+++ b/prelude/core/quantifier_props.lp
@@ -1,16 +1,16 @@
 require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
 
-definition exists (T: Type) (p : eta T ⇒ eta bool) ≔
+definition exists {T: Type} (p : eta T ⇒ eta bool) ≔
     (bnot (all T (λ x, (bnot (p x)))))
 
-theorem exists_not :
-  ∀ T : Type,
-  ∀ p : eta T ⇒ eta bool,
-  eps (eq bool (exists T (λ x, ¬ (p x))) (¬ (all T p)))
-proof admit
+set declared "∃"
+definition ∃ {T: Type} ≔ @exists T
+
+theorem exists_not (T: Type) (p: η T ⇒ η bool):
+  ε (eq (∃ (λ x, ¬ (p x))) (¬ (all T p)))
+proof
+admit
 
-theorem exists_or (T: Type) (p q: eta T ⇒ eta bool):
-  eps (eq bool
-        (exists T (λ x, (p x) ∨ (q x)))
-        ((exists T p) ∨ (exists T q)))
-  proof admit
+theorem exists_or (T: Type) (p q: η T ⇒ η bool):
+  ε (eq (∃ (λ x, (p x) ∨ (q x))) ((∃ p) ∨ (∃ q)))
+proof admit
diff --git a/prelude/core/xor_def.lp b/prelude/core/xor_def.lp
index 0ef531873c82059e3fd56cbb0a8fa782added8ce..14c8dc00c94458fe69f06e9f023b8d0bd13f5acc 100644
--- a/prelude/core/xor_def.lp
+++ b/prelude/core/xor_def.lp
@@ -1,3 +1,7 @@
 require open encodings.pvs_core prelude.core.booleans prelude.core.notequal
+prelude.core.equalities prelude.core.if_def
 
-definition xor (A : eta bool) (B : eta bool) ≔ neq bool A B
+definition xor (A : η bool) (B : η bool) ≔ neq A B
+
+theorem xor_def (A B: η bool) : ε (eq (xor A B) (if A (¬ B) B))
+proof admit