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 //
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