X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fformal_topology%2Fcprop_connectives.ma;h=af183d0f656bf7c32fc847b9b087e615213193ea;hb=77f07b39ced234d0aea7526e6c5bfc713515dc58;hp=7d24790ae6b79b5ff96e6cb17c844217400dfab7;hpb=bc477154d15f6979c948f9af602199af547d193e;p=helm.git

diff --git a/matita/matita/lib/formal_topology/cprop_connectives.ma b/matita/matita/lib/formal_topology/cprop_connectives.ma
index 7d24790ae..af183d0f6 100644
--- 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).