-
-(*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