X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Flib%2Fbasics%2Fpts.ma;h=1b87a2d0b18e1dc2d5e16d228f4a9d5bf78fc79e;hb=4173283e148199871d787c53c0301891deb90713;hp=16f34ddb1d6abede235129403f80b2a337e7e880;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/matita/lib/basics/pts.ma b/matitaB/matita/lib/basics/pts.ma
index 16f34ddb1..1b87a2d0b 100644
--- a/matitaB/matita/lib/basics/pts.ma
+++ b/matitaB/matita/lib/basics/pts.ma
@@ -19,7 +19,7 @@ universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
 universe constraint Type[3] < Type[4].
 
-inductive True : Prop ≝ I : True.
+(*inductive True : Prop ≝ I : True.
 
 (*lemma fa : ∀X:Prop.X → X.
 #X #p //
@@ -32,9 +32,10 @@ lemma ggr ≝ fa.*)
 inductive False : Prop ≝ .
 
 inductive bool : Prop ≝ True : bool | false : bool.
-
+ 
 inductive eq (A:Type[1]) (x:A) : A → Prop ≝
     refl: eq A x x.
 
-lemma provable_True : True → eq bool True True.
-@ 
+lemma provable_True : <A href="cic:/matita/basics/pts/True.ind(1,0,0)">True</A> → eq Prop True True.
+#H %
+qed.*)
\ No newline at end of file