milestone in basic_2

[helm.git] / matitaB / matita / lib / basics / pts.ma

diff --git a/matitaB/matita/lib/basics/pts.ma b/matitaB/matita/lib/basics/pts.ma
index 94f49fc5c33c939e0faa8366cd9ae2b9c5aacf3d..1b87a2d0b18e1dc2d5e16d228f4a9d5bf78fc79e 100644 (file)
--- a/matitaB/matita/lib/basics/pts.ma
+++ b/matitaB/matita/lib/basics/pts.ma
@@ -18,3 +18,24 @@ universe constraint Type[0] < Type[1].
 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