From 6a307c85a54dbab351ca2e64376003627c58a8c3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 1 Dec 2008 12:43:00 +0000
Subject: [PATCH] all done

---
 .../exercises/natural_deduction_fst_order.ma  | 28 ++++++++++++++-----
 1 file changed, 21 insertions(+), 7 deletions(-)

diff --git a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
index 790c4b2fc..9022b8d03 100644
--- a/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
+++ b/helm/software/matita/library/didactic/exercises/natural_deduction_fst_order.ma
@@ -66,12 +66,22 @@ axiom Q : sort → CProp.
 axiom R : sort →sort → CProp.
 axiom S : sort →sort → CProp.
 
+(* assumiamo il terzo escluso *)
 axiom EM : ∀A:CProp.A ∨ ¬A.
 
 (* intuizionista *)
 lemma ex1: ¬(∃x.P x) ⇒ ∀x.¬ P x.
 apply rule (prove (¬(∃x.P x) ⇒ ∀x.¬ P x));
-apply rule (discharge [x]);
+(*BEGIN*)
+apply rule (⇒_i [h1] (∀x.¬ P x));
+apply rule (∀_i {l} (¬P l));
+apply rule (¬_i [h2] (⊥));
+apply rule (¬_e (¬(∃x.P x)) (∃x.P x));
+	[ apply rule (discharge [h1]);
+	| apply rule (∃_i {l} (P l));
+	  apply rule (discharge [h2]);
+	]
+(*END*)
 qed.
 
 (* classico *)
@@ -96,7 +106,16 @@ qed.
 (* intuizionista *)
 lemma ex3: ((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c.
 apply rule (prove (((∃x.P x) ⇒ Q c) ⇒ ∀x.P x ⇒ Q c));
-apply rule (discharge [x]);
+(*BEGIN*)
+apply rule (⇒_i [h1] (∀x.P x ⇒ Q c));
+apply rule (∀_i {l} (P l ⇒ Q c));
+apply rule (⇒_i [h2] (Q c));
+apply rule (⇒_e ((∃x.P x) ⇒ Q c) (∃x.P x));
+	[ apply rule (discharge [h1]);
+	| apply rule (∃_i {l} (P l));
+	  apply rule (discharge [h2]);
+	]
+(*END*)
 qed.
 
 (* classico *)
@@ -126,8 +145,3 @@ apply rule (∨_e ((∀x.P x) ∨ ¬(∀x.P x)) [h3] (?) [h3] (?));
   ]
 (*END*)
 qed.
-
-
-
-
-
-- 
2.39.2