all done

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 790c4b2fc946e522235335e33f17d05525be4e3a..9022b8d039b82a75a747434d9249f25f1c62baf5 100644 (file)
--- 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.
-
-
-
-
-