(**************************************************************************)
-(* ___ *)
+(* ___ *)
(* ||M|| *)
(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
+(* ||T|| *)
+(* ||I|| Developers: *)
(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
(* ||A|| E.Tassi, S.Zacchiroli *)
(* \ / *)
(* \ / This file is distributed under the terms of the *)
-(* v GNU Lesser General Public License Version 2.1 *)
+(* v GNU Lesser General Public License Version 2.1 *)
(* *)
(**************************************************************************)
inductive False: Prop \def .
definition Not: Prop \to Prop \def
-\lambda A:Prop. (A \to False).
+\lambda A. (A \to False).
theorem absurd : \forall A,C:Prop. A \to Not A \to C.
-intros.cut False.elim Hcut.apply H1.assumption.
+intros. elim (H1 H).
qed.
inductive And (A,B:Prop) : Prop \def
match n with
[ O \Rightarrow O
| (S p) \Rightarrow
- [\lambda n:nat.nat] match m with
+ match m with
[O \Rightarrow (S p)
| (S q) \Rightarrow minus p q ]].
match n with
[ O \Rightarrow true
| (S p) \Rightarrow
- [\lambda n:nat.bool] match m with
+ match m with
[ O \Rightarrow false
| (S q) \Rightarrow leb p q]].
simplify.intros.apply H.apply le_S_n.assumption.
qed.
+(*CSC: this requires too much time
theorem prova :
let three \def (S (S (S O))) in
let nine \def (times three three) in
intro.
intro.
intro.intro.
-STOP normalize goal at (? ? % ?).
-
-
+normalize goal at (? ? % ?).
+*)
\ No newline at end of file