X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Fpts.ma;h=b7d9a5da9deb592e73670182de1459befd569321;hb=0bf47116203bc07de95643f389e228e0d59cab6b;hp=1b87a2d0b18e1dc2d5e16d228f4a9d5bf78fc79e;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/basics/pts.ma b/weblib/basics/pts.ma
index 1b87a2d0b..b7d9a5da9 100644
--- a/weblib/basics/pts.ma
+++ b/weblib/basics/pts.ma
@@ -19,23 +19,3 @@ universe constraint Type[1] < Type[2].
 universe constraint Type[2] < Type[3].
 universe constraint Type[3] < Type[4].
 
-(*inductive True : Prop ≝ I : True.
-
-(*lemma fa : ∀X:Prop.X → X.
-#X #p //
-qed.
-
-(* check fa*)
-
-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 : <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