From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 15 Nov 2008 14:33:49 +0000 (+0000)
Subject: rules fixed
X-Git-Tag: make_still_working~4557
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=214b87039cc59cc6ecb5a54cf68b296b0a3ada92;p=helm.git

rules fixed
---

diff --git a/helm/software/matita/library/demo/natural_deduction.ma b/helm/software/matita/library/demo/natural_deduction.ma
index 64b3daccb..14359325b 100644
--- a/helm/software/matita/library/demo/natural_deduction.ma
+++ b/helm/software/matita/library/demo/natural_deduction.ma
@@ -12,115 +12,67 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "demo/natural_deduction_support.ma".
+include "didactic/support/natural_deduction.ma".
 
 lemma RAA_to_EM : A ∨ ¬ A.
 
-  apply (prove (A ∨ ¬ A));
+  apply rule (prove (A ∨ ¬ A));
   
-  apply (RAA [H] ⊥);
-  apply (¬_e (¬A) A);
-    [ apply (¬_i [H1] ⊥);
-      apply (¬_e (¬(A∨¬A)) (A∨¬A));
-      [ apply [H];
-      | apply (∨_i_l A);
-        apply [H1];
+  apply rule (RAA [H] ⊥);
+  apply rule (¬_e (¬A) A);
+    [ apply rule (¬_i [H1] ⊥);
+      apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply rule (discharge [H]);
+      | apply rule (∨_i_l A);
+        apply rule (discharge [H1]);
       ]
-    | apply (RAA [H2] ⊥);
-      apply (¬_e (¬(A∨¬A)) (A∨¬A));
-      [ apply [H];
-      | apply (∨_i_r (¬A));
-        apply [H2];
+    | apply rule (RAA [H2] ⊥);
+      apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply rule (discharge [H]);
+      | apply rule (∨_i_r (¬A));
+        apply rule (discharge [H2]);
       ]
     ]
 qed.
 
 lemma RA_to_EM1 : A ∨ ¬ A.
 
-  apply (prove (A ∨ ¬ A));
+  apply rule (prove (A ∨ ¬ A));
   
-  apply (RAA [H] ⊥);
-  apply (¬_e (¬¬A) (¬A));
-    [ apply (¬_i [H2] ⊥);
-      apply (¬_e (¬(A∨¬A)) (A∨¬A));
-      [ apply [H];
-      | apply (∨_i_r (¬A));
-        apply [H2];
+  apply rule (RAA [H] ⊥);
+  apply rule (¬_e (¬¬A) (¬A));
+    [ apply rule (¬_i [H2] ⊥);
+      apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply rule (discharge [H]);
+      | apply rule (∨_i_r (¬A));
+        apply rule (discharge [H2]);
       ]
-    | apply (¬_i [H1] ⊥);
-      apply (¬_e (¬(A∨¬A)) (A∨¬A));
-      [ apply [H];
-      | apply (∨_i_l A);
-        apply [H1];
+    | apply rule (¬_i [H1] ⊥);
+      apply rule (¬_e (¬(A∨¬A)) (A∨¬A));
+      [ apply rule (discharge [H]);
+      | apply rule (∨_i_l A);
+        apply rule (discharge [H1]);
       ]
     ]
 qed.
 
-lemma ex0 : (A ⇒ ⊥) ⇒ A ⇒ B ∧ ⊤. 
- 
-  apply (prove ((A ⇒ ⊥) ⇒ A ⇒ B∧⊤));
-  
-  apply (⇒_i [H] (A ⇒ B∧⊤));
-  apply (⇒_i [H1] (B∧⊤));
-  apply (∧_i B ⊤);
-  [ apply (⊥_e ⊥);
-    apply (⇒_e (A ⇒ ⊥) A); 
-    [ apply [H];
-    | apply [H1];
-    ]
-  | apply (⊤_i);
-  ]
-qed.
-
 lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
 
- apply (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
+ apply rule (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));
    
- apply (⇒_i [H] (A∧C⇒E∧C∨B));
- apply (⇒_i [K] (E∧C∨B));
- apply (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
-[ apply [H];
-| apply (∨_i_l (E∧C));
-  apply (∧_i E C);
-  [ apply (⇒_e (A⇒E) A);
-    [ apply [C1];
-    | apply (∧_e_l (A∧C)); apply [K];
+ apply rule (⇒_i [H] (A∧C⇒E∧C∨B));
+ apply rule (⇒_i [K] (E∧C∨B));
+ apply rule (∨_e ((A⇒E)∨B) [C1] (E∧C∨B) [C2] (E∧C∨B));
+[ apply rule (discharge [H]);
+| apply rule (∨_i_l (E∧C));
+  apply rule (∧_i E C);
+  [ apply rule (⇒_e (A⇒E) A);
+    [ apply rule (discharge [C1]);
+    | apply rule (∧_e_l (A∧C)); apply rule (discharge [K]);
     ]
-  | apply (∧_e_r (A∧C)); apply [K];
+  | apply rule (∧_e_r (A∧C)); apply rule (discharge [K]);
   ]
-| apply (∨_i_r B); apply [C2];
+| apply rule (∨_i_r B); apply rule (discharge [C2]);
 ]
 qed.
 
-lemma dmg : ¬(A ∨ B) ⇒ ¬A ∧ ¬B.
-
-  apply (prove (¬(A ∨ B) ⇒ ¬A ∧ ¬B));
-  apply (⇒_i [H] (¬A ∧ ¬B));
-  
-  apply (¬_e (¬A) A);
-  
-  
-
-
-(*
-lemma ex2: ΠN:Type.ΠR:N→N→CProp.
-
-   (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
-   
- intros (N R);apply (prove ((∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y));
- 
- apply (⇒_i [H] (∀z:N.(∃x:N.R x z)⇒∃y:N.R z y));
- apply (∀_i [z] ((∃x:N.R x z)⇒∃y:N.R z y));
- apply (⇒_i [H2] (∃y:N.R z y));
- apply (∃_e (∃x:N.R x z) [n] [H3] (∃y:N.R z y));
-  [ apply [H2]
-  | apply (∃_i n (R z n));
-    apply (⇒_e (R n z ⇒ R z n) (R n z));
-     [ apply (∀_e (∀b:N.R n b ⇒ R b n) z);
-       apply (∀_e (∀a:N.∀b:N.R a b ⇒ R b a) n);
-       apply [H]
-     | apply [H3]
-     ]
-  ]
-qed.
-*)
\ No newline at end of file
diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends
index 27032d916..aa370ab69 100644
--- a/helm/software/matita/library/depends
+++ b/helm/software/matita/library/depends
@@ -19,12 +19,13 @@ Q/q/qinv.ma Q/q/q.ma Q/ratio/rinv.ma
 nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma
 list/in.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma
 datatypes/compare.ma 
+didactic/exercises/substitution.ma nat/minus.ma
 nat/factorization2.ma list/list.ma nat/factorization.ma nat/sieve.ma
 formal_topology/basic_topologies.ma datatypes/categories.ma formal_topology/relations.ma formal_topology/saturations_reductions.ma
 logic/connectives.ma 
 Q/nat_fact/times.ma nat/factorization.ma
 decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma
-demo/natural_deduction_support.ma 
+didactic/exercises/duality.ma nat/minus.ma
 nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma
 nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma
 nat/times.ma nat/plus.ma
@@ -50,10 +51,12 @@ nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma
 demo/realisability.ma datatypes/constructors.ma logic/connectives.ma
 list/list.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma nat/orders.ma nat/plus.ma
 nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma
+didactic/support/natural_deduction.ma 
 nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma
 nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma
 formal_topology/basic_pairs.ma datatypes/categories.ma formal_topology/relations.ma
 Q/frac.ma Q/q/q.ma Q/q/qinv.ma nat/factorization.ma nat/nat.ma
+didactic/exercises/shannon.ma nat/minus.ma
 Q/q/qtimes.ma Q/q/qinv.ma Q/ratio/rtimes.ma
 formal_topology/concrete_spaces.ma formal_topology/basic_pairs.ma
 nat/minus.ma nat/compare.ma nat/le_arith.ma
@@ -69,8 +72,8 @@ formal_topology/relations.ma datatypes/subsets.ma
 nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma
 Z/moebius.ma Z/sigma_p.ma nat/factorization.ma
 demo/toolbox.ma logic/cprop_connectives.ma
-nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
 logic/coimplication.ma logic/connectives.ma
+nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma
 nat/minimization.ma nat/minus.ma
 logic/connectives2.ma higher_order_defs/relations.ma
 datatypes/subsets.ma datatypes/categories.ma logic/cprop_connectives.ma
@@ -80,10 +83,10 @@ Q/q/q.ma Q/fraction/numerator_denominator.ma Q/ratio/ratio.ma
 nat/bertrand.ma list/in.ma list/sort.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sieve.ma nat/sqrt.ma
 nat/nat.ma higher_order_defs/functions.ma
 Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma
-demo/natural_deduction.ma 
+demo/natural_deduction.ma didactic/support/natural_deduction.ma
 higher_order_defs/ordering.ma logic/equality.ma
-nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
 logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma
+nat/congruence.ma nat/primes.ma nat/relevant_equations.ma
 nat/gcd.ma nat/lt_arith.ma nat/primes.ma
 datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma
 Z/compare.ma Z/orders.ma nat/compare.ma
diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index 3969197e9..99e047a9d 100644
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -40,7 +40,7 @@ definition Not_intro : ∀A.(A → Bot) → Not A ≝  λA.
 definition Not_elim : ∀A.Not A → A → Bot ≝ λA. 
   Imply_elim ? Bot.  
 
-definition assumpt := λA:CProp.λa:A.
+definition Discharge := λA:CProp.λa:A.
   a.
 
 axiom Raa : ∀A.(Not A → Bot) → A.
@@ -90,36 +90,52 @@ axiom X : CProp.
 axiom Y : CProp.
 axiom Z : CProp.
 
-(* Every formula user provided annotates its proof A becomes (show A ?) *)
+(* Every formula user provided annotates its proof:
+   `A` becomes `(show A ?)` *)
 definition show : ∀A.A→A ≝ λA:CProp.λa:A.a.
 
 (* When something does not fit, this daemon is used *)
 axiom cast: ∀A,B:CProp.B → A.
 
+(* Leaves *)
+notation < "\infrule (t\atop ⋮) a ?" with precedence 19
+for @{ 'leaf_ok $a $t }.
+interpretation "leaf OK" 'leaf_ok a t = (show a t).
+notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 
+for @{ 'leaf_ko $a $t }.
+interpretation "leaf KO" 'leaf_ko a t = (cast _ a (show _ t)).
 
+(* begin a proof: draws the root *)
 notation > "'prove' p" non associative with precedence 19 
 for @{ 'prove $p }.
 interpretation "prove KO" 'prove p = (cast _ _ (show p _)).
 interpretation "prove OK" 'prove p = (show p _).
 
-notation < "\infrule (t\atop ⋮) a ?" with precedence 19 for @{ 'leaf_ok $a $t }.
-interpretation "leaf OK" 'leaf_ok a t = (show a t).
-notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (a) ?" with precedence 19 for @{ 'leaf_ko $a $t }.
-interpretation "leaf KO" 'leaf_ko a t = (cast _ a (show _ t)).
-
-notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 for @{ 'assumpt_ko $a $H }.
-interpretation "assumption_ko 1" 'assumpt_ko a H = (show a (cast _ _ (assumpt _ H))).
-interpretation "assumption_ko 2" 'assumpt_ko a H = (cast _ _ (show a (cast _ _ (assumpt _ H)))).
-
-notation < "[ a ] \sup H" with precedence 19 for @{ 'assumpt_ok $a $H }.
-interpretation "assumption_ok 1" 'assumpt_ok a H = (show a (assumpt a H)).
-notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 for @{ 'assumpt_ok_2 $a $H }.
-interpretation "assumption_ok 2" 'assumpt_ok_2 a H = (cast _ _ (show a (assumpt a H))).
-
-notation > "[H]" with precedence 90 for @{ 'assumpt $H }.
-interpretation "assumpt KO" 'assumpt H = (cast _ _ (assumpt _ H)).
-interpretation "assumpt OK" 'assumpt H = (assumpt _ H).
-
+(* discharging *)
+notation < "[ a ] \sup mstyle color #ff0000 (H)" with precedence 19 
+for @{ 'discharge_ko_1 $a $H }.
+interpretation "discharge_ko_1" 'discharge_ko_1 a H = 
+  (show a (cast _ _ (Discharge _ H))).
+notation < "[ mstyle color #ff0000 (a) ] \sup mstyle color #ff0000 (H)" with precedence 19 
+for @{ 'discharge_ko_2 $a $H }.
+interpretation "discharge_ko_2" 'discharge_ko_2 a H = 
+  (cast _ _ (show a (cast _ _ (Discharge _ H)))).
+
+notation < "[ a ] \sup H" with precedence 19 
+for @{ 'discharge_ok_1 $a $H }.
+interpretation "discharge_ok_1" 'discharge_ok_1 a H = 
+  (show a (Discharge _ H)).
+notation < "[ mstyle color #ff0000 (a) ] \sup H" with precedence 19 
+for @{ 'discharge_ok_2 $a $H }.
+interpretation "discharge_ok_2" 'discharge_ok_2 a H = 
+  (cast _ _ (show a (Discharge _ H))).
+
+notation > "'discharge' [H]" with precedence 19 
+for @{ 'discharge $H }.
+interpretation "discharge KO" 'discharge H = (cast _ _ (Discharge _ H)).
+interpretation "discharge OK" 'discharge H = (Discharge _ H).
+
+(* ⇒ introduction *)
 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 for @{ 'Imply_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b = 
@@ -127,7 +143,7 @@ interpretation "Imply_intro_ko_1" 'Imply_intro_ko_1 ab \eta.b =
 
 notation < "\infrule hbox(\emsp b \emsp) mstyle color #ff0000 (ab) (mstyle color #ff0000 (⇒\sub\i \emsp) ident H) " with precedence 19
 for @{ 'Imply_intro_ko_2 $ab (λ${ident H}:$p.$b) }.
-interpretation "Imply_intro_ko_1" 'Imply_intro_ko_2 ab \eta.b = 
+interpretation "Imply_intro_ko_2" 'Imply_intro_ko_2 ab \eta.b = 
   (cast _ _ (show ab (cast _ _ (Imply_intro _ _ b)))).
 
 notation < "\infrule hbox(\emsp b \emsp) ab (⇒\sub\i \emsp ident H) " with precedence 19
@@ -142,15 +158,21 @@ interpretation "Imply_intro_ok_2" 'Imply_intro_ok_2 ab \eta.b =
 
 notation > "⇒_'i' [ident H] term 90 b" with precedence 19
 for @{ 'Imply_intro $b (λ${ident H}.show $b ?) }.
-interpretation "Imply_intro KO" 'Imply_intro b pb = (cast _ (Imply unit b) (Imply_intro _ b pb)).
-interpretation "Imply_intro OK" 'Imply_intro b pb = (Imply_intro _ b pb).
-
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_1 $ab $a $b }.
+interpretation "Imply_intro KO" 'Imply_intro b pb = 
+  (cast _ (Imply unit b) (Imply_intro _ b pb)).
+interpretation "Imply_intro OK" 'Imply_intro b pb = 
+  (Imply_intro _ b pb).
+
+(* ⇒ elimination *)
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (⇒\sub\e) " with precedence 19
+for @{ 'Imply_elim_ko_1 $ab $a $b }.
 interpretation "Imply_elim_ko_1" 'Imply_elim_ko_1 ab a b = 
-  (show b (cast _ _ (Imply_elim _ _ ab a))).
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 for @{ 'Imply_elim_ko_2 $ab $a $b }.
+  (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a)))).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (⇒\sub\e) " with precedence 19 
+for @{ 'Imply_elim_ko_2 $ab $a $b }.
 interpretation "Imply_elim_ko_2" 'Imply_elim_ko_2 ab a b = 
-  (cast _ _ (show b (cast _ _ (Imply_elim _ _ ab a)))).
+  (cast _ _ (show b (cast _ _ (Imply_elim _ _ (cast _ _ ab) (cast _ _ a))))).
 
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (⇒\sub\e) " with precedence 19 
 for @{ 'Imply_elim_ok_1 $ab $a $b }.
@@ -162,14 +184,21 @@ for @{ 'Imply_elim_ok_2 $ab $a $b }.
 interpretation "Imply_elim_ok_2" 'Imply_elim_ok_2 ab a b = 
   (cast _ _ (show b (Imply_elim _ _ ab a))).
 
-notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
-interpretation "Imply_elim KO" 'Imply_elim ab a = (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
-interpretation "Imply_elim OK" 'Imply_elim ab a = (Imply_elim _ _ ab a). 
+notation > "⇒_'e' term 90 ab term 90 a" with precedence 19 
+for @{ 'Imply_elim (show $ab ?) (show $a ?) }.
+interpretation "Imply_elim KO" 'Imply_elim ab a = 
+  (cast _ _ (Imply_elim _ _ (cast (Imply unit unit) _ ab) (cast unit _ a))).
+interpretation "Imply_elim OK" 'Imply_elim ab a = 
+  (Imply_elim _ _ ab a). 
 
-notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_1 $a $b $ab }.
+(* ∧ introduction *)
+notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) ab mstyle color #ff0000 (∧\sub\i)" with precedence 19 
+for @{ 'And_intro_ko_1 $a $b $ab }.
 interpretation "And_intro_ko_1" 'And_intro_ko_1 a b ab = 
   (show ab (cast _ _ (And_intro _ _ a b))).
-notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 for @{ 'And_intro_ko_2 $a $b $ab }.
+
+notation < "\infrule hbox(\emsp a \emsp\emsp\emsp b \emsp) mstyle color #ff0000 (ab) mstyle color #ff0000 (∧\sub\i)" with precedence 19 
+for @{ 'And_intro_ko_2 $a $b $ab }.
 interpretation "And_intro_ko_2" 'And_intro_ko_2 a b ab = 
   (cast _ _ (show ab (cast _ _ (And_intro _ _ a b)))).
 
@@ -183,19 +212,21 @@ for @{ 'And_intro_ok_2 $a $b $ab }.
 interpretation "And_intro_ok_2" 'And_intro_ok_2 a b ab = 
   (cast _ _ (show ab (And_intro _ _ a b))).
 
-notation > "∧_'i' term 90 a term 90 b" with precedence 19 for @{ 'And_intro (show $a ?) (show $b ?) }.
+notation > "∧_'i' term 90 a term 90 b" with precedence 19 
+for @{ 'And_intro (show $a ?) (show $b ?) }.
 interpretation "And_intro KO" 'And_intro a b = (cast _ _ (And_intro _ _ a b)).
 interpretation "And_intro OK" 'And_intro a b = (And_intro _ _ a b).
 
+(* ∧ elimination *)
 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 
 for @{ 'And_elim_l_ko_1 $ab $a }.
 interpretation "And_elim_l_ko_1" 'And_elim_l_ko_1 ab a = 
-  (show a (cast _ _ (And_elim_l _ _ ab))).
+  (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab)))).
 
 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\l))" with precedence 19 
 for @{ 'And_elim_l_ko_2 $ab $a }.
 interpretation "And_elim_l_ko_2" 'And_elim_l_ko_2 ab a = 
-  (cast _ _ (show a (cast _ _ (And_elim_l _ _ ab)))).
+  (cast _ _ (show a (cast _ _ (And_elim_l _ _ (cast _ _ ab))))).
 
 notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\l))" with precedence 19 
 for @{ 'And_elim_l_ok_1 $ab $a }.
@@ -209,18 +240,18 @@ interpretation "And_elim_l_ok_2" 'And_elim_l_ok_2 ab a =
 
 notation > "∧_'e_l' term 90 ab" with precedence 19
 for @{ 'And_elim_l (show $ab ?) }.
-interpretation "And_elim_l KO" 'And_elim_l a = (And_elim_l _ _ (cast (And _ unit) _ a)).
+interpretation "And_elim_l KO" 'And_elim_l a = (cast _ _ (And_elim_l _ _ (cast (And unit unit) _ a))).
 interpretation "And_elim_l OK" 'And_elim_l a = (And_elim_l _ _ a).
 
 notation < "\infrule hbox(\emsp ab \emsp) a mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 
 for @{ 'And_elim_r_ko_1 $ab $a }.
 interpretation "And_elim_r_ko_1" 'And_elim_r_ko_1 ab a = 
-  (show a (cast _ _ (And_elim_r _ _ ab))).
+  (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab)))).
 
 notation < "\infrule hbox(\emsp ab \emsp) mstyle color #ff0000 (a) mstyle color #ff0000 (∧\sub(\e_\r))" with precedence 19 
 for @{ 'And_elim_r_ko_2 $ab $a }.
 interpretation "And_elim_r_ko_2" 'And_elim_r_ko_2 ab a = 
-  (cast _ _ (show a (cast _ _ (And_elim_r _ _ ab)))).
+  (cast _ _ (show a (cast _ _ (And_elim_r _ _ (cast _ _ ab))))).
 
 notation < "\infrule hbox(\emsp ab \emsp) a (∧\sub(\e_\r))" with precedence 19 
 for @{ 'And_elim_r_ok_1 $ab $a }.
@@ -234,19 +265,10 @@ interpretation "And_elim_r_ok_2" 'And_elim_r_ok_2 ab a =
 
 notation > "∧_'e_r' term 90 ab" with precedence 19
 for @{ 'And_elim_r (show $ab ?) }.
-interpretation "And_elim_r KO" 'And_elim_r a = (And_elim_r _ _ (cast (And unit _) _ a)).
+interpretation "And_elim_r KO" 'And_elim_r a = (cast _ _ (And_elim_r _ _ (cast (And unit unit) _ a))).
 interpretation "And_elim_r OK" 'And_elim_r a = (And_elim_r _ _ a).
 
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19 
-for @{ 'Or_intro_l_ok_1 $a $ab }.
-interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = 
-  (show ab (Or_intro_l _ _ a)).
-
-notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 
-for @{ 'Or_intro_l_ok_1 $a $ab }.
-interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = 
-  (cast _ _ (show ab (Or_intro_l _ _ a))).
-
+(* ∨ introduction *)
 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\l))" with precedence 19 
 for @{ 'Or_intro_l_ko_1 $a $ab }.
 interpretation "Or_intro_l_ko_1" 'Or_intro_l_ko_1 a ab = 
@@ -257,21 +279,21 @@ for @{ 'Or_intro_l_ko_2 $a $ab }.
 interpretation "Or_intro_l_ko_2" 'Or_intro_l_ko_2 a ab = 
   (cast _ _ (show ab (cast _ _ (Or_intro_l _ _ a)))).
 
+notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\l))" with precedence 19 
+for @{ 'Or_intro_l_ok_1 $a $ab }.
+interpretation "Or_intro_l_ok_1" 'Or_intro_l_ok_1 a ab = 
+  (show ab (Or_intro_l _ _ a)).
+
+notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\l))" with precedence 19 
+for @{ 'Or_intro_l_ok_1 $a $ab }.
+interpretation "Or_intro_l_ok_2" 'Or_intro_l_ok_2 a ab = 
+  (cast _ _ (show ab (Or_intro_l _ _ a))).
+
 notation > "∨_'i_l' term 90 a" with precedence 19
 for @{ 'Or_intro_l (show $a ?) }.
 interpretation "Or_intro_l KO" 'Or_intro_l a = (cast _ (Or _ unit) (Or_intro_l _ _ a)).
 interpretation "Or_intro_l OK" 'Or_intro_l a = (Or_intro_l _ _ a). 
   
-notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19 
-for @{ 'Or_intro_r_ok_1 $a $ab }.
-interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab = 
-  (show ab (Or_intro_r _ _ a)).
-
-notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 
-for @{ 'Or_intro_r_ok_1 $a $ab }.
-interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = 
-  (cast _ _ (show ab (Or_intro_r _ _ a))).
-
 notation < "\infrule hbox(\emsp a \emsp) ab mstyle color #ff0000 (∨\sub(\i_\r))" with precedence 19 
 for @{ 'Or_intro_r_ko_1 $a $ab }.
 interpretation "Or_intro_r_ko_1" 'Or_intro_r_ko_1 a ab = 
@@ -282,11 +304,32 @@ for @{ 'Or_intro_r_ko_2 $a $ab }.
 interpretation "Or_intro_r_ko_2" 'Or_intro_r_ko_2 a ab = 
   (cast _ _ (show ab (cast _ _ (Or_intro_r _ _ a)))).
 
+notation < "\infrule hbox(\emsp a \emsp) ab (∨\sub(\i_\r))" with precedence 19 
+for @{ 'Or_intro_r_ok_1 $a $ab }.
+interpretation "Or_intro_r_ok_1" 'Or_intro_r_ok_1 a ab = 
+  (show ab (Or_intro_r _ _ a)).
+
+notation < "\infrule hbox(\emsp a \emsp) mstyle color #ff0000 (ab) (∨\sub(\i_\r))" with precedence 19 
+for @{ 'Or_intro_r_ok_1 $a $ab }.
+interpretation "Or_intro_r_ok_2" 'Or_intro_r_ok_2 a ab = 
+  (cast _ _ (show ab (Or_intro_r _ _ a))).
+
 notation > "∨_'i_r' term 90 a" with precedence 19
 for @{ 'Or_intro_r (show $a ?) }.
 interpretation "Or_intro_r KO" 'Or_intro_r a = (cast _ (Or unit _) (Or_intro_r _ _ a)).
 interpretation "Or_intro_r OK" 'Or_intro_r a = (Or_intro_r _ _ a). 
 
+(* ∨ elimination *)
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19
+for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
+interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = 
+  (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc)))).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19
+for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
+interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = 
+  (cast _ _ (show c (cast _ _ (Or_elim _ _ _ (cast _ _ ab) (cast _ _ ac) (cast _ _ bc))))).
+
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (∨\sub\e \emsp ident Ha \emsp ident Hb)" with precedence 19
 for @{ 'Or_elim_ok_1 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 interpretation "Or_elim_ok_1" 'Or_elim_ok_1 ab \eta.ac \eta.bc c = 
@@ -297,49 +340,67 @@ for @{ 'Or_elim_ok_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
 interpretation "Or_elim_ok_2" 'Or_elim_ok_2 ab \eta.ac \eta.bc c = 
   (cast _ _ (show c (Or_elim _ _ _ ab ac bc))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) c (mstyle color #ff0000 (∨\sub\e \emsp) ident Ha \emsp ident Hb)" with precedence 19
-for @{ 'Or_elim_ko_1 $ab $c (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) }.
-interpretation "Or_elim_ko_1" 'Or_elim_ko_1 ab c \eta.ac \eta.bc = 
-  (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc)))).
-
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp ac \emsp\emsp\emsp bc \emsp) mstyle color #ff0000 (c) (mstyle color #ff0000 (∨\sub\e) \emsp ident Ha \emsp ident Hb)" with precedence 19
-for @{ 'Or_elim_ko_2 $ab (λ${ident Ha}:$ta.$ac) (λ${ident Hb}:$tb.$bc) $c }.
-interpretation "Or_elim_ko_2" 'Or_elim_ko_2 ab \eta.ac \eta.bc c = 
-  (cast _ _ (show c (cast _ _ (Or_elim _ _ _ ab (cast _ _ ac) (cast _ _ bc))))).
-
 definition unit_to ≝ λx:CProp.unit → x.
 
 notation > "∨_'e' term 90 ab [ident Ha] term 90 cl [ident Hb] term 90 cr" with precedence 19
-for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) $cl $cr }.
-interpretation "Or_elim KO" 'Or_elim ab ac bc c1 c2 = 
-  (cast _ _ (Or_elim _ _ _ (cast (Or unit unit) _ ab) (cast (unit_to unit) (unit_to _) ac) (cast (unit_to unit) (unit_to _) bc))).
-interpretation "Or_elim OK" 'Or_elim ab ac bc c1 c2 = (Or_elim _ _ _ ab ac bc).
-
+for @{ 'Or_elim (show $ab ?) (λ${ident Ha}.show $cl ?) (λ${ident Hb}.show $cr ?) }.
+interpretation "Or_elim KO" 'Or_elim ab ac bc = 
+  (cast _ _ (Or_elim _ _ _ 
+    (cast (Or unit unit) _ ab) 
+    (cast (unit_to unit) (unit_to _) ac) 
+    (cast (unit_to unit) (unit_to _) bc))).
+interpretation "Or_elim OK" 'Or_elim ab ac bc = (Or_elim _ _ _ ab ac bc).
+
+(* ⊤ introduction *)
 notation < "\infrule \nbsp ⊤ mstyle color #ff0000 (⊤\sub\i)" with precedence 19 
 for @{'Top_intro_ko_1}.
-interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = (show _ (cast _ _ Top_intro)).
+interpretation "Top_intro_ko_1" 'Top_intro_ko_1 = 
+  (show _ (cast _ _ Top_intro)).
+
+notation < "\infrule \nbsp mstyle color #ff0000 (⊤) mstyle color #ff0000 (⊤\sub\i)" with precedence 19 
+for @{'Top_intro_ko_2}.
+interpretation "Top_intro_ko_2" 'Top_intro_ko_2 = 
+  (cast _ _ (show _ (cast _ _ Top_intro))).
 
 notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 
 for @{'Top_intro_ok_1}.
 interpretation "Top_intro_ok_1" 'Top_intro_ok_1 = (show _ Top_intro).
 
+notation < "\infrule \nbsp ⊤ (⊤\sub\i)" with precedence 19 
+for @{'Top_intro_ok_2 }.
+interpretation "Top_intro_ok_2" 'Top_intro_ok_2 = (cast _ _ (show _ Top_intro)).
+
 notation > "⊤_'i'" with precedence 19 for @{ 'Top_intro }.
 interpretation "Top_intro KO" 'Top_intro = (cast _ _ Top_intro).
 interpretation "Top_intro OK" 'Top_intro = Top_intro.
 
-notation < "\infrule b a (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ok_1 $a $b}.
+(* ⊥ introduction *)
+notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 
+for @{'Bot_elim_ko_1 $a $b}.
+interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = 
+  (show a (Bot_elim _ (cast _ _ b))).
+
+notation < "\infrule b mstyle color #ff0000 (a) mstyle color #ff0000 (⊥\sub\e)" with precedence 19 
+for @{'Bot_elim_ko_2 $a $b}.
+interpretation "Bot_elim_ko_2" 'Bot_elim_ko_2 a b = 
+  (cast _ _ (show a (Bot_elim _ (cast _ _ b)))).
+
+notation < "\infrule b a (⊥\sub\e)" with precedence 19 
+for @{'Bot_elim_ok_1 $a $b}.
 interpretation "Bot_elim_ok_1" 'Bot_elim_ok_1 a b = 
-  (show a (Bot_elim a b)).
+  (show a (Bot_elim _ b)).
 
-notation < "\infrule b a mstyle color #ff0000 (⊥\sub\e)" with precedence 19 for @{'Bot_elim_ko_1 $a $b}.
-interpretation "Bot_elim_ko_1" 'Bot_elim_ko_1 a b = 
-  (show a (Bot_elim a (cast _ _ b))).
+notation < "\infrule b mstyle color #ff0000 (a) (⊥\sub\e)" with precedence 19 
+for @{'Bot_elim_ok_2 $a $b}.
+interpretation "Bot_elim_ok_2" 'Bot_elim_ok_2 a b = 
+  (cast _ _ (show a (Bot_elim _ b))).
 
 notation > "⊥_'e' term 90 b" with precedence 19 
 for @{ 'Bot_elim (show $b ?) }.
 interpretation "Bot_elim KO" 'Bot_elim a = (Bot_elim _ (cast _ _ a)).  
 interpretation "Bot_elim OK" 'Bot_elim a = (Bot_elim _ a).
 
+(* ¬ introduction *)
 notation < "\infrule hbox(\emsp b \emsp) ab (mstyle color #ff0000 (\lnot\sub\i) \emsp ident H)" with precedence 19
 for @{ 'Not_intro_ko_1 $ab (λ${ident H}:$p.$b) }.
 interpretation "Not_intro_ko_1" 'Not_intro_ko_1 ab \eta.b = 
@@ -365,6 +426,17 @@ for @{ 'Not_intro (λ${ident H}.show $b ?) }.
 interpretation "Not_intro KO" 'Not_intro a = (cast _ _ (Not_intro _ (cast _ _ a))).
 interpretation "Not_intro OK" 'Not_intro a = (Not_intro _ a).
 
+(* ¬ elimination *)
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
+for @{ 'Not_elim_ko_1 $ab $a $b }.
+interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = 
+  (show b (cast _ _ (Not_elim _ (cast _ _ ab) a))).
+
+notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
+for @{ 'Not_elim_ko_2 $ab $a $b }.
+interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = 
+  (cast _ _ (show b (cast _ _ (Not_elim _ (cast _ _ ab) a)))).
+
 notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b (\lnot\sub\e) " with precedence 19 
 for @{ 'Not_elim_ok_1 $ab $a $b }.
 interpretation "Not_elim_ok_1" 'Not_elim_ok_1 ab a b = 
@@ -375,21 +447,22 @@ for @{ 'Not_elim_ok_2 $ab $a $b }.
 interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b = 
   (cast _ _ (show b (Not_elim _ ab a))).
 
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) b mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
-for @{ 'Not_elim_ko_1 $ab $a $b }.
-interpretation "Not_elim_ko_1" 'Not_elim_ko_1 ab a b = 
-  (show b (Not_elim _ (cast _ _ ab) a)).
-
-notation < "\infrule hbox(\emsp ab \emsp\emsp\emsp a\emsp) mstyle color #ff0000 (b) mstyle color #ff0000 (\lnot\sub\e) " with precedence 19 
-for @{ 'Not_elim_ko_2 $ab $a $b }.
-interpretation "Not_elim_ko_2" 'Not_elim_ko_2 ab a b = 
-  (cast _ _ (show b (Not_elim _ (cast _ _ ab) a))).
-
 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
-interpretation "Not_elim KO" 'Not_elim ab a = (Not_elim _ (cast _ _ ab) a).
+interpretation "Not_elim KO" 'Not_elim ab a = (cast _ unit (Not_elim _ (cast _ _ ab) a)).
 interpretation "Not_elim OK" 'Not_elim ab a = (Not_elim _ ab a).
 
+(* RAA *)
+notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
+for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
+interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = 
+  (show Pn (cast _ _ (Raa _ (cast _ _ Px)))).
+
+notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
+for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
+interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = 
+  (cast _ _ (show Pn (cast _ _ (Raa _ (cast _ _ Px))))).
+
 notation < "\infrule hbox(\emsp Px \emsp) Pn (\RAA \emsp ident x)" with precedence 19
 for @{ 'RAA_ok_1 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "RAA_ok_1" 'RAA_ok_1 Px Pn = 
@@ -400,37 +473,57 @@ for @{ 'RAA_ok_2 (λ${ident x}:$tx.$Px) $Pn }.
 interpretation "RAA_ok_2" 'RAA_ok_2 Px Pn = 
   (cast _ _ (show Pn (Raa _ Px))).
 
-notation < "\infrule hbox(\emsp Px \emsp) Pn (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
-for @{ 'RAA_ko_1 (λ${ident x}:$tx.$Px) $Pn }.
-interpretation "RAA_ko_1" 'RAA_ko_1 Px Pn = 
-  (show Pn (Raa _ (cast _ _ Px))).
-
-notation < "\infrule hbox(\emsp Px \emsp) mstyle color #ff0000 (Pn) (mstyle color #ff0000 (\RAA) \emsp ident x)" with precedence 19
-for @{ 'RAA_ko_2 (λ${ident x}:$tx.$Px) $Pn }.
-interpretation "RAA_ko_2" 'RAA_ko_2 Px Pn = 
-  (cast _ _ (show Pn (Raa _ (cast _ _ Px)))).
-
 notation > "'RAA' [ident H] term 90 b" with precedence 19 
 for @{ 'Raa (λ${ident H}.show $b ?) }. 
-interpretation "RAA KO" 'Raa p = (Raa _ (cast _ (unit_to _) p)).
+interpretation "RAA KO" 'Raa p = (cast _ unit (Raa _ (cast _ (unit_to _) p))).
 interpretation "RAA OK" 'Raa p = (Raa _ p).
 
 (*DOCBEGIN
-Templates for rules
-⇒_i […] (…)
-∧_i (…) (…)
-∨_i_l (…)
-∨_i_r (…)
-¬_i […] (…)
-⊤_i
-⇒_e (…) (…)
-∧_e_l (…)
-∧_e_r (…)
-∨_e (…) […] (…) […] (…)
-¬_e (…) (…)
-⊥_e (…)
-prove (…)
-RAA […] (…)
+Templates for rules:
+
+        apply rule (⇒_i […] (…)).
+
+        apply rule (∧_i (…) (…));
+        	[
+        	|
+        	]
+
+        apply rule (∨_i_l (…)).
+
+        apply rule (∨_i_r (…)).
+
+        apply rule (¬_i […] (…)).
+
+        apply rule (⊤_i).
+
+        apply rule (⇒_e (…) (…));
+        	[
+        	|
+        	]
+
+        apply rule (∧_e_l (…)).
+
+        apply rule (∧_e_r (…)).
+
+        apply rule (∨_e (…) […] (…) […] (…));
+        	[
+        	|
+        	|
+        	]
+
+        apply rule (¬_e (…) (…));
+        	[
+        	|
+        	]
+
+        apply rule (⊥_e (…)).
+
+        apply rule (prove (…)).
+
+        apply rule (RAA […] (…)).
+
+        apply rule (discharge […]).
+
 DOCEND*)
 
 
diff --git a/helm/software/matita/matita.glade b/helm/software/matita/matita.glade
index 2b239b4e5..2447b2881 100644
--- a/helm/software/matita/matita.glade
+++ b/helm/software/matita/matita.glade
@@ -1387,6 +1387,7 @@
                     <child>
                       <widget class="GtkHBox" id="hbox18">
                         <property name="visible">True</property>
+                        <property name="spacing">2</property>
                         <child>
                           <widget class="GtkHandleBox" id="TacticsButtonsHandlebox">
                             <property name="visible">True</property>
@@ -1608,6 +1609,18 @@
                                             <property name="position">1</property>
                                           </packing>
                                         </child>
+                                        <child>
+                                          <widget class="GtkButton" id="butDischarge">
+                                            <property name="visible">True</property>
+                                            <property name="can_focus">True</property>
+                                            <property name="receives_default">True</property>
+                                            <property name="label" translatable="yes">Discharge (discharge [  ])</property>
+                                            <property name="response_id">0</property>
+                                          </widget>
+                                          <packing>
+                                            <property name="position">2</property>
+                                          </packing>
+                                        </child>
                                       </widget>
                                     </child>
                                     <child>
@@ -2337,6 +2350,59 @@
         <property name="n_rows">3</property>
         <property name="n_columns">2</property>
         <property name="row_spacing">5</property>
+        <child>
+          <widget class="GtkLabel" id="label17">
+            <property name="visible">True</property>
+            <property name="xalign">0</property>
+            <property name="label" translatable="yes">Find:</property>
+          </widget>
+          <packing>
+            <property name="x_options"></property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkLabel" id="label18">
+            <property name="visible">True</property>
+            <property name="xalign">0</property>
+            <property name="label" translatable="yes">Replace with: </property>
+          </widget>
+          <packing>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="x_options"></property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkEntry" id="findEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="has_focus">True</property>
+            <property name="can_default">True</property>
+            <property name="has_default">True</property>
+            <property name="invisible_char">*</property>
+          </widget>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
+        <child>
+          <widget class="GtkEntry" id="replaceEntry">
+            <property name="visible">True</property>
+            <property name="can_focus">True</property>
+            <property name="invisible_char">*</property>
+          </widget>
+          <packing>
+            <property name="left_attach">1</property>
+            <property name="right_attach">2</property>
+            <property name="top_attach">1</property>
+            <property name="bottom_attach">2</property>
+            <property name="y_options"></property>
+          </packing>
+        </child>
         <child>
           <widget class="GtkHBox" id="hbox19">
             <property name="visible">True</property>
@@ -2435,59 +2501,6 @@
             <property name="y_padding">5</property>
           </packing>
         </child>
-        <child>
-          <widget class="GtkEntry" id="replaceEntry">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="invisible_char">*</property>
-          </widget>
-          <packing>
-            <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkEntry" id="findEntry">
-            <property name="visible">True</property>
-            <property name="can_focus">True</property>
-            <property name="has_focus">True</property>
-            <property name="can_default">True</property>
-            <property name="has_default">True</property>
-            <property name="invisible_char">*</property>
-          </widget>
-          <packing>
-            <property name="left_attach">1</property>
-            <property name="right_attach">2</property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkLabel" id="label18">
-            <property name="visible">True</property>
-            <property name="xalign">0</property>
-            <property name="label" translatable="yes">Replace with: </property>
-          </widget>
-          <packing>
-            <property name="top_attach">1</property>
-            <property name="bottom_attach">2</property>
-            <property name="x_options"></property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
-        <child>
-          <widget class="GtkLabel" id="label17">
-            <property name="visible">True</property>
-            <property name="xalign">0</property>
-            <property name="label" translatable="yes">Find:</property>
-          </widget>
-          <packing>
-            <property name="x_options"></property>
-            <property name="y_options"></property>
-          </packing>
-        </child>
       </widget>
     </child>
   </widget>
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 393da7cef..6acf7357a 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -762,25 +762,25 @@ class gui () =
           else main#tacticsButtonsHandlebox#misc#hide ())
         ~check:main#menuitemPalette;
       connect_button main#butImpl_intro
-        (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
+        (fun () -> source_buffer#insert "apply rule (⇒_i […] (…)).\n");
       connect_button main#butAnd_intro
         (fun () -> source_buffer#insert 
           "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butOr_intro_left
-        (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n");
+        (fun () -> source_buffer#insert "apply rule (∨_i_l (…)).\n");
       connect_button main#butOr_intro_right
-        (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
+        (fun () -> source_buffer#insert "apply rule (∨_i_r (…)).\n");
       connect_button main#butNot_intro
-        (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
+        (fun () -> source_buffer#insert "apply rule (¬_i […] (…)).\n");
       connect_button main#butTop_intro
-        (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
+        (fun () -> source_buffer#insert "apply rule (⊤_i).\n");
       connect_button main#butImpl_elim
         (fun () -> source_buffer#insert 
           "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butAnd_elim_left
-        (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n");
+        (fun () -> source_buffer#insert "apply rule (∧_e_l (…)).\n");
       connect_button main#butAnd_elim_right
-        (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
+        (fun () -> source_buffer#insert "apply rule (∧_e_r (…)).\n");
       connect_button main#butOr_elim
         (fun () -> source_buffer#insert 
           "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
@@ -788,11 +788,14 @@ class gui () =
         (fun () -> source_buffer#insert 
           "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n");
       connect_button main#butBot_elim
-        (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
+        (fun () -> source_buffer#insert "apply rule (⊥_e (…)).\n");
       connect_button main#butRAA
-        (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
+        (fun () -> source_buffer#insert "apply rule (RAA […] (…)).\n");
       connect_button main#butStart
-        (fun () -> source_buffer#insert "apply rule (prove (…));\n");
+        (fun () -> source_buffer#insert "apply rule (prove (…)).\n");
+      connect_button main#butDischarge
+        (fun () -> source_buffer#insert "apply rule (discharge […]).\n");
+
     
       (* TO BE REMOVED *)
       main#scriptNotebook#remove_page 1;