update in ground_2

[helm.git] / matita / matita / lib / formal_topology / cprop_connectives.ma

diff --git a/matita/matita/lib/formal_topology/cprop_connectives.ma b/matita/matita/lib/formal_topology/cprop_connectives.ma
index 7d24790ae6b79b5ff96e6cb17c844217400dfab7..af183d0f656bf7c32fc847b9b087e615213193ea 100644 (file)
--- a/matita/matita/lib/formal_topology/cprop_connectives.ma
+++ b/matita/matita/lib/formal_topology/cprop_connectives.ma
@@ -16,13 +16,6 @@ include "basics/pts.ma".
 
 inductive False: CProp[0] ≝.
 
-interpretation "constructive logical false" 'false = False.
-
-inductive True: CProp[0] ≝  
-I : True.
-
-interpretation "constructive logical true" 'true = True.
-
 inductive Or (A,B:CProp[0]) : CProp[0] ≝
  | Left : A → Or A B
  | Right : B → Or A B.
@@ -138,7 +131,7 @@ inductive exT2 (A:Type[0]) (P,Q:A→CProp[0]) : CProp[0] ≝
   ex_introT2: ∀w:A. P w → Q w → exT2 A P Q.
 
 
-definition Not : CProp[0] → CProp[0] ≝ λx:CProp[0].x → ⊥.
+definition Not : CProp[0] → CProp[0] ≝ λx:CProp[0].x → False.
 
 interpretation "constructive not" 'not x = (Not x).