From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Nov 2005 15:43:07 +0000 (+0000)
Subject: Yet another semantics for simplify.
X-Git-Tag: V_0_7_2_3~101
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=400b07e007cfbb0b4ce5ed77cfc50f227c491310;p=helm.git

Yet another semantics for simplify.
---

diff --git a/helm/matita/library/Q/q.ma b/helm/matita/library/Q/q.ma
index d69e459ac..340154979 100644
--- a/helm/matita/library/Q/q.ma
+++ b/helm/matita/library/Q/q.ma
@@ -92,13 +92,13 @@ definition ftl \def
     | (cons x f) \Rightarrow f].
     
 theorem injective_pp : injective nat fraction pp.
-simplify.intros.
+unfold injective.intros.
 change with ((aux (pp x)) = (aux (pp y))).
 apply eq_f.assumption.
 qed.
 
 theorem injective_nn : injective nat fraction nn.
-simplify.intros.
+unfold injective.intros.
 change with ((aux (nn x)) = (aux (nn y))).
 apply eq_f.assumption.
 qed.
@@ -118,7 +118,7 @@ apply eq_f.assumption.
 qed.
 
 theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
-intros.simplify. intro.
+intros.unfold Not. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True
@@ -130,7 +130,7 @@ qed.
 theorem not_eq_pp_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
 pp n \neq cons x f.
-intros.simplify. intro.
+intros.unfold Not. intro.
 change with match (pp n) with
 [ (pp n) \Rightarrow False
 | (nn n) \Rightarrow True
@@ -142,7 +142,7 @@ qed.
 theorem not_eq_nn_cons: 
 \forall n:nat.\forall x:Z. \forall f:fraction. 
 nn n \neq cons x f.
-intros.simplify. intro.
+intros.unfold Not. intro.
 change with match (nn n) with
 [ (pp n) \Rightarrow True
 | (nn n) \Rightarrow False
@@ -153,7 +153,7 @@ qed.
 
 theorem decidable_eq_fraction: \forall f,g:fraction.
 decidable (f = g).
-intros.simplify.
+intros.unfold decidable.
 apply (fraction_elim2 (\lambda f,g. f=g \lor (f=g \to False))).
   intros.elim g1.
     elim ((decidable_eq_nat n n1) : n=n1 \lor (n=n1 \to False)).
@@ -188,16 +188,16 @@ intros.apply (fraction_elim2
   intros.elim g1.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
-      intro.simplify.intro.apply H.apply injective_pp.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply injective_pp.assumption.
     simplify.apply not_eq_pp_nn.
     simplify.apply not_eq_pp_cons.
   intros.elim g1.
-    simplify.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
+    simplify.unfold Not.intro.apply (not_eq_pp_nn n1 n).apply sym_eq. assumption.
     simplify.apply eqb_elim.intro.simplify.apply eq_f.assumption.
-    intro.simplify.intro.apply H.apply injective_nn.assumption.
+    intro.simplify.unfold Not.intro.apply H.apply injective_nn.assumption.
   simplify.apply not_eq_nn_cons.
-  intros.simplify.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
-  intros.simplify.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
+  intros.simplify.unfold Not.intro.apply (not_eq_pp_cons m x f1).apply sym_eq. assumption.
+  intros.simplify.unfold Not.intro.apply (not_eq_nn_cons m x f1).apply sym_eq. assumption.
   intros.
    change in match (eqfb (cons x f1) (cons y g1)) 
    with (andb (eqZb x y) (eqfb f1 g1)).
@@ -205,8 +205,8 @@ intros.apply (fraction_elim2
       intro.generalize in match H.elim (eqfb f1 g1).
         simplify.apply eq_f2.assumption.
         apply H2.
-      simplify.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
-      intro.simplify.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
+      simplify.unfold Not.intro.apply H2.apply (eq_cons_to_eq2 x y).assumption.
+      intro.simplify.unfold Not.intro.apply H1.apply (eq_cons_to_eq1 f1 g1).assumption.
 qed.
 
 let rec finv f \def
@@ -243,7 +243,7 @@ let rec ftimes f g \def
         | (frac h) \Rightarrow frac (cons (x + y) h)]]].
         
 theorem symmetric2_ftimes: symmetric2 fraction ratio ftimes.
-simplify. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
+unfold symmetric2. intros.apply (fraction_elim2 (\lambda f,g.ftimes f g = ftimes g f)).
   intros.elim g.
     change with (Z_to_ratio (pos n + pos n1) = Z_to_ratio (pos n1 + pos n)).
      apply eq_f.apply sym_Zplus.
diff --git a/helm/matita/library/Z/compare.ma b/helm/matita/library/Z/compare.ma
index a59100885..4a5025975 100644
--- a/helm/matita/library/Z/compare.ma
+++ b/helm/matita/library/Z/compare.ma
@@ -49,17 +49,17 @@ elim x.
     simplify.apply not_eq_OZ_pos.
     simplify.apply not_eq_OZ_neg.
   elim y.
-    simplify.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
-      intro.simplify.intro.apply H.apply inj_pos.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply inj_pos.assumption.
     simplify.apply not_eq_pos_neg.
   elim y.
-    simplify.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
-    simplify.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
+    simplify.unfold Not.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
     simplify.apply eqb_elim.
       intro.simplify.apply eq_f.assumption.
-      intro.simplify.intro.apply H.apply inj_neg.assumption.
+      intro.simplify.unfold Not.intro.apply H.apply inj_neg.assumption.
 qed.
 
 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 186533ea0..c39f69308 100644
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -71,9 +71,9 @@ theorem irreflexive_Zlt: irreflexive Z Zlt.
 change with (\forall x:Z. x < x \to False).
 intro.elim x.exact H.
 cut (neg n < neg n \to False).
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 cut (pos n < pos n \to False).
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 qed.
 
 theorem irrefl_Zlt: irreflexive Z Zlt
diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 27266bf39..e5e1cdb45 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -140,7 +140,7 @@ reflexivity.
 (* we now close all positivity conditions *)
 apply lt_O_times_S_S.                    
 apply lt_O_times_S_S.
-simplify.
+simplify.unfold lt.
 apply le_SO_minus.  exact H.
 qed.
 
diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index d1a846da4..d18c80b23 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -54,15 +54,15 @@ match OZ_test z with
 |false \Rightarrow z \neq OZ].
 intros.elim z.
 simplify.reflexivity.
-simplify.intros (H).
+simplify. unfold Not. intros (H).
 discriminate H.
-simplify.intros (H).
+simplify. unfold Not. intros (H).
 discriminate H.
 qed.
 
 (* discrimination *)
 theorem injective_pos: injective nat Z pos.
-simplify.
+unfold injective.
 intros.
 change with (abs (pos x) = abs (pos y)).
 apply eq_f.assumption.
@@ -72,7 +72,7 @@ variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
 \def injective_pos.
 
 theorem injective_neg: injective nat Z neg.
-simplify.
+unfold injective.
 intros.
 change with (abs (neg x) = abs (neg y)).
 apply eq_f.assumption.
@@ -82,22 +82,22 @@ variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
 \def injective_neg.
 
 theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
-simplify.intros (n H).
+unfold Not.intros (n H).
 discriminate H.
 qed.
 
 theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
-simplify.intros (n H).
+unfold Not.intros (n H).
 discriminate H.
 qed.
 
 theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
-simplify.intros (n m H).
+unfold Not.intros (n m H).
 discriminate H.
 qed.
 
 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
-intros.simplify.
+intros.unfold decidable.
 elim x.
 (* goal: x=OZ *)
   elim y.
@@ -110,25 +110,25 @@ elim x.
 (* goal: x=pos *)
   elim y.
   (* goal: x=pos y=OZ *)
-    right.intro.
+    right.unfold Not.intro.
     apply (not_eq_OZ_pos n). symmetry. assumption.
   (* goal: x=pos y=pos *)
     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.
-    right.intros (H_inj).apply H. injection H_inj. assumption.
+    right.unfold Not.intros (H_inj).apply H. injection H_inj. assumption.
   (* goal: x=pos y=neg *)
-    right.intro.apply (not_eq_pos_neg n n1). assumption.
+    right.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption.
 (* goal: x=neg *)
   elim y.
   (* goal: x=neg y=OZ *)
-    right.intro.
+    right.unfold Not.intro.
     apply (not_eq_OZ_neg n). symmetry. assumption.
   (* goal: x=neg y=pos *)
-    right. intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
+    right. unfold Not.intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
   (* goal: x=neg y=neg *)
     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
     left.apply eq_f.assumption.
-    right.intro.apply H.apply injective_neg.assumption.
+    right.unfold Not.intro.apply H.apply injective_neg.assumption.
 qed.
 
 (* end discrimination *)
diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index 11f1d7a8c..f4aec8167 100644
--- a/helm/matita/library/datatypes/bool.ma
+++ b/helm/matita/library/datatypes/bool.ma
@@ -32,7 +32,7 @@ theorem bool_elim: \forall P:bool \to Prop. \forall b:bool.
 qed.
 
 theorem not_eq_true_false : true \neq false.
-simplify.intro.
+unfold Not.intro.
 change with 
 match true with
 [ true \Rightarrow False
diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index 2d60662a4..1cc127759 100644
--- a/helm/matita/library/list/sort.ma
+++ b/helm/matita/library/list/sort.ma
@@ -74,7 +74,8 @@ lemma ordered_injective:
       [ generalize in match Hcut; 
         apply andb_elim;
         elim (le s s1);
-        [ change with (ordered A le (s1::l2) = true \to ordered A le (s1::l2) = true).
+        [ simplify;
+          fold simplify (ordered ? le (s1::l2));
           intros; assumption;
         | simplify;
           intros (Habsurd);
@@ -96,11 +97,11 @@ lemma insert_sorted:
     ordered A le l = true \to ordered A le (insert A le x l) = true.
   intros 5 (A le H l x).
   elim l;
-  [ 2: change with (ordered A le (match le x s with
-         [ true ⇒ x::(s::l1) | false ⇒ s::(insert A le x l1) ]) = true).
+  [ 2: simplify;
        apply (bool_elim ? (le x s));
        [ intros;
-         change with ((le x s \land ordered A le (s::l1)) = true);
+         simplify;
+         fold simplify (ordered ? le (s::l1));
          apply andb_elim;
          rewrite > H3;
          assumption;
@@ -112,22 +113,25 @@ lemma insert_sorted:
          [ simplify;
            rewrite > (H x a H2);
            reflexivity;
-         | change with ((ordered A le (a::match le x s with
-              [ true ⇒ x::s::l2 | false ⇒ s::(insert A le x l2) ])) = true).
+         | simplify in \vdash (? ? (? ? ? %) ?);
             apply (bool_elim ? (le x s));
             [ intros;
-              change with ((le a x \land (le x s \land ordered A le (s::l2))) = true).
+              simplify;
+              fold simplify (ordered A le (s::l2));
               apply andb_elim;
               rewrite > (H x a H3);
-              change with ((le x s \land ordered A le (s::l2)) = true).
+              simplify;
+              fold simplify (ordered A le (s::l2));
               apply andb_elim;
               rewrite > H4;
               apply (ordered_injective A le (a::s::l2));
               assumption;
             | intros;
-              change with ((le a s \land ordered A le (s::(insert A le x l2))) = true);
+              simplify;
+              fold simplify (ordered A le (s::(insert A le x l2)));
               apply andb_elim;
-              change in H2 with ((le a s \land ordered A le (s::l2)) = true); 
+              simplify in H2;
+              fold simplify (ordered A le (s::l2)) in H2;
               generalize in match H2;
               apply (andb_elim (le a s));
               elim (le a s);
diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 40157d849..b87dc6c95 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -41,14 +41,14 @@ simplify.intros.apply refl_eq.
 qed.
     
 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
-simplify.intros.elim H. apply refl_eq.
+unfold symmetric.intros.elim H. apply refl_eq.
 qed.
 
 theorem sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
 \def symmetric_eq.
 
 theorem transitive_eq : \forall A:Type. transitive A (eq A).
-simplify.intros.elim H1.assumption.
+unfold transitive.intros.elim H1.assumption.
 qed.
 
 theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma
index f14f16d27..30cc7440f 100644
--- a/helm/matita/library/nat/chinese_reminder.ma
+++ b/helm/matita/library/nat/chinese_reminder.ma
@@ -53,7 +53,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* congruent to b *)
 cut (a2*m = a1*n - (S O)).
@@ -84,7 +84,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* and now the symmetric case; the price to pay for working
    in nat instead than Z *)
@@ -119,7 +119,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* congruent to a *)
 cut (a2*m = a1*n + (S O)).
@@ -149,7 +149,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* proof of the cut *)
 rewrite < H2.
diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma
index e85a80265..264731580 100644
--- a/helm/matita/library/nat/compare.ma
+++ b/helm/matita/library/nat/compare.ma
@@ -42,13 +42,13 @@ intro.elim n1.
 simplify.reflexivity.
 simplify.apply not_eq_O_S.
 intro.
-simplify.
+simplify.unfold Not.
 intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
 intros.simplify.
 generalize in match H.
 elim ((eqb n1 m1)).
 simplify.apply eq_f.apply H1.
-simplify.intro.apply H1.apply inj_S.assumption.
+simplify.unfold Not.intro.apply H1.apply inj_S.assumption.
 qed.
 
 theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
@@ -126,7 +126,7 @@ simplify.exact le_O_n.
 simplify.exact not_le_Sn_O.
 intros 2.simplify.elim ((leb n1 m1)).
 simplify.apply le_S_S.apply H.
-simplify.intros.apply H.apply le_S_S_to_le.assumption.
+simplify.unfold Not.intros.apply H.apply le_S_S_to_le.assumption.
 qed.
 
 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. 
@@ -191,12 +191,12 @@ apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with
   | EQ \Rightarrow n=m
   | GT \Rightarrow m < n ])).
 intro.elim n1.simplify.reflexivity.
-simplify.apply le_S_S.apply le_O_n.
-intro.simplify.apply le_S_S. apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
+intro.simplify.unfold lt.apply le_S_S. apply le_O_n.
 intros 2.simplify.elim ((nat_compare n1 m1)).
-simplify. apply le_S_S.apply H.
+simplify. unfold lt. apply le_S_S.apply H.
 simplify. apply eq_f. apply H.
-simplify. apply le_S_S.apply H.
+simplify. unfold lt.apply le_S_S.apply H.
 qed.
 
 theorem nat_compare_n_m_m_n: \forall n,m:nat. 
diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma
index 60bdbadc4..20913fa60 100644
--- a/helm/matita/library/nat/count.ma
+++ b/helm/matita/library/nat/count.ma
@@ -78,7 +78,7 @@ rewrite < plus_n_O.
 rewrite < H.
 rewrite > (S_pred ((S n1)*(S m))).
 apply sigma_plus1.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.
@@ -138,15 +138,15 @@ rewrite > (div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n))
                                         ((i1*(S n) + i) \mod (S n)) i1 i).
 rewrite > H3.
 apply bool_to_nat_andb.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
 apply div_mod_spec_div_mod.
-simplify.apply le_S_S.apply le_O_n.
-constructor 1.simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+constructor 1.unfold lt.apply le_S_S.assumption.
 reflexivity.
 apply div_mod_spec_div_mod.
-simplify.apply le_S_S.apply le_O_n.
-constructor 1.simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+constructor 1.unfold lt.apply le_S_S.assumption.
 reflexivity.
 apply (trans_eq ? ? 
 (sigma n (\lambda n.((bool_to_nat (f1 n)) *
@@ -170,13 +170,13 @@ rewrite < S_pred in \vdash (? ? %).
 change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
 apply H.
 apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? i).
 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.
@@ -184,12 +184,12 @@ rewrite > plus_n_O in \vdash (? ? %).
 rewrite > sym_times. assumption.
 rewrite > (times_n_O O).
 apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 rewrite > (times_n_O O).
 apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 rewrite < plus_n_O.
 unfold injn.
 intros.
@@ -206,40 +206,40 @@ rewrite < (H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3) in \vdash (? ? (? % ?) ?).
 rewrite < (H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5).
 rewrite < (H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5) in \vdash (? ? ? (? % ?)).
 rewrite > H6.reflexivity.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? j).
 rewrite > (div_mod j (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 rewrite < sym_times. assumption.
 apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 apply (lt_times_to_lt_l n).
 apply (le_to_lt_to_lt ? i).
 rewrite > (div_mod i (S n)) in \vdash (? ? %).
 rewrite > sym_plus.
 apply le_plus_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 rewrite < sym_times. assumption.
 apply lt_mod_m_m.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
 rewrite > (times_n_O O).
 apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 unfold lt.
 rewrite > S_pred in \vdash (? ? %).
 apply le_S_S.assumption.
 rewrite > (times_n_O O).
 apply lt_times.
-simplify. apply le_S_S.apply le_O_n.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 intros.
 apply False_ind.
 apply (not_le_Sn_O m1 H4).
diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma
index 9995830a9..e9831f82a 100644
--- a/helm/matita/library/nat/div_and_mod.ma
+++ b/helm/matita/library/nat/div_and_mod.ma
@@ -70,7 +70,7 @@ qed.
 theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m.
 intros 2.elim m.apply False_ind.
 apply (not_le_Sn_O O H).
-simplify.apply le_S_S.apply le_mod_aux_m_m.
+simplify.unfold lt.apply le_S_S.apply le_mod_aux_m_m.
 apply le_n.
 qed.
 
@@ -108,7 +108,7 @@ definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
 *)
 
 theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
-intros 4.simplify.intros.elim H.absurd (le (S r) O).
+intros 4.unfold Not.intros.elim H.absurd (le (S r) O).
 rewrite < H1.assumption.
 exact (not_le_Sn_O r).
 qed.
@@ -188,7 +188,7 @@ qed.
 
 theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
 intros.constructor 1.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < plus_n_O.rewrite < sym_times.reflexivity.
 qed.
 
@@ -198,7 +198,7 @@ intros.
 apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
 goal 15. (* ?11 is closed with the following tactics *)
 apply div_mod_spec_div_mod.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 apply div_mod_spec_times.
 qed.
 
diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index 49e3bbd70..11d84f74c 100644
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -48,14 +48,14 @@ rewrite < times_n_Sm.reflexivity.
 qed.
 
 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
-intros.elim m.simplify.apply le_n.
-simplify.rewrite > times_n_SO.
+intros.elim m.simplify.unfold lt.apply le_n.
+simplify.unfold lt.rewrite > times_n_SO.
 apply le_times.assumption.assumption.
 qed.
 
 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
-intros.elim m.simplify.reflexivity.
-simplify.
+intros.elim m.simplify.unfold lt.reflexivity.
+simplify.unfold lt.
 apply (trans_le ? ((S(S O))*(S n1))).
 simplify.
 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
@@ -83,7 +83,7 @@ intros.apply eq_f.
 apply H1.
 (* esprimere inj_times senza S *)
 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
-apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
+apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
 assumption.
 intros 2.
 apply (nat_case n).
diff --git a/helm/matita/library/nat/factorial.ma b/helm/matita/library/nat/factorial.ma
index 22a799d07..14217bbcb 100644
--- a/helm/matita/library/nat/factorial.ma
+++ b/helm/matita/library/nat/factorial.ma
@@ -52,10 +52,10 @@ intro.apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S(S O)) H).
 intros.change with ((S m) < (S m)*m!).
 apply (lt_to_le_to_lt ? ((S m)*(S (S O)))).
 rewrite < sym_times.
-simplify.
+simplify.unfold lt.
 apply le_S_S.rewrite < plus_n_O.
 apply le_plus_n.
 apply le_times_r.apply le_SSO_fact.
-simplify.apply le_S_S_to_le.exact H.
+simplify.unfold lt.apply le_S_S_to_le.exact H.
 qed.
 
diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index b64e3733b..6a3094303 100644
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -40,10 +40,10 @@ rewrite > H1. apply le_smallest_factor_n.
 rewrite > H1.
 change with (divides_b (smallest_factor n) n = true).
 apply divides_to_divides_b_true.
-apply (trans_lt ? (S O)).simplify. apply le_n.
+apply (trans_lt ? (S O)).unfold lt. apply le_n.
 apply lt_SO_smallest_factor.assumption.
 apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 apply prime_to_nth_prime.
 apply prime_smallest_factor_n.assumption.
 qed.
@@ -167,7 +167,7 @@ match f with
 
 theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 O < defactorize_aux f i.
-intro.elim f.simplify.
+intro.elim f.simplify.unfold lt. 
 rewrite > times_n_SO.
 apply le_times.
 change with (O < nth_prime i).
@@ -175,7 +175,7 @@ apply lt_O_nth_prime_n.
 change with (O < exp (nth_prime i) n).
 apply lt_O_exp.
 apply lt_O_nth_prime_n.
-simplify.
+simplify.unfold lt.
 rewrite > times_n_SO.
 apply le_times.
 change with (O < exp (nth_prime i) n).
@@ -187,7 +187,7 @@ qed.
 
 theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
 S O < defactorize_aux f i.
-intro.elim f.simplify.
+intro.elim f.simplify.unfold lt.
 rewrite > times_n_SO.
 apply le_times.
 change with (S O < nth_prime i).
@@ -195,7 +195,7 @@ apply lt_SO_nth_prime_n.
 change with (O < exp (nth_prime i) n).
 apply lt_O_exp.
 apply lt_O_nth_prime_n.
-simplify.
+simplify.unfold lt.
 rewrite > times_n_SO.
 rewrite > sym_times.
 apply le_times.
@@ -233,7 +233,7 @@ rewrite < Hcut.reflexivity.
 cut (O < r \lor O = r).
 elim Hcut1.assumption.absurd (n1 = O).
 rewrite > Hcut.rewrite < H4.reflexivity.
-simplify. intro.apply (not_le_Sn_O O).
+unfold Not. intro.apply (not_le_Sn_O O).
 rewrite < H5 in \vdash (? ? %).assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 cut ((S O) < r \lor (S O) \nlt r).
@@ -251,11 +251,11 @@ cut (r=(S O)).
 apply (nat_case n).
 left.split.assumption.reflexivity.
 intro.right.rewrite > Hcut2.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
 cut (r \lt (S O) \or r=(S O)).
 elim Hcut2.absurd (O=r).
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
-simplify.intro.
+unfold Not.intro.
 cut (O=n1).
 apply (not_le_Sn_O O).
 rewrite > Hcut3 in \vdash (? ? %).
@@ -309,14 +309,14 @@ cut (O < q \lor O = q).
 elim Hcut2.assumption.
 absurd (nth_prime p \divides S (S m1)).
 apply (divides_max_prime_factor_n (S (S m1))).
-simplify.apply le_S_S.apply le_S_S. apply le_O_n.
+unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
 cut ((S(S m1)) = r).
 rewrite > Hcut3 in \vdash (? (? ? %)).
 change with (nth_prime p \divides r \to False).
 intro.
 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
 apply lt_SO_nth_prime_n.
-simplify.apply le_S_S.apply le_O_n.apply le_n.
+unfold lt.apply le_S_S.apply le_O_n.apply le_n.
 assumption.
 apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
 rewrite > times_n_SO in \vdash (? ? ? %).
@@ -330,18 +330,18 @@ cut ((S O) < r \lor S O \nlt r).
 elim Hcut2.
 right. 
 apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).
-simplify.apply le_S_S. apply le_O_n.
+unfold lt.apply le_S_S. apply le_O_n.
 apply le_n.
 assumption.assumption.
 cut (r=(S O)).
 apply (nat_case p).
 left.split.assumption.reflexivity.
 intro.right.rewrite > Hcut3.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
 cut (r \lt (S O) \or r=(S O)).
 elim Hcut3.absurd (O=r).
 apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
-simplify.intro.
+unfold Not.intro.
 apply (not_le_Sn_O O).
 rewrite > H3 in \vdash (? ? %).assumption.assumption.
 apply (le_to_or_lt_eq r (S O)).
@@ -406,11 +406,11 @@ theorem divides_exp_to_eq:
 \forall p,q,m:nat. prime p \to prime q \to
 p \divides q \sup m \to p = q.
 intros.
-simplify in H1.
+unfold prime in H1.
 elim H1.apply H4.
 apply (divides_exp_to_divides p q m).
 assumption.assumption.
-simplify in H.elim H.assumption.
+unfold prime in H.elim H.assumption.
 qed.
 
 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
@@ -442,7 +442,7 @@ cut (i = j).
 apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
 apply (injective_nth_prime ? ? H4).
 apply (H i (S j)).
-apply (trans_lt ? j).assumption.simplify.apply le_n.
+apply (trans_lt ? j).assumption.unfold lt.apply le_n.
 assumption.
 apply divides_times_to_divides.
 apply prime_nth_prime.assumption.
@@ -473,10 +473,10 @@ qed.
 lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
 \lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
 intros.
-simplify.rewrite < plus_n_O.
+simplify.unfold Not.rewrite < plus_n_O.
 intro.
 apply (not_divides_defactorize_aux f i (S i) ?).
-simplify.apply le_n.
+unfold lt.apply le_n.
 rewrite > H.
 rewrite > assoc_times.
 apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).
diff --git a/helm/matita/library/nat/fermat_little_theorem.ma b/helm/matita/library/nat/fermat_little_theorem.ma
index bbd5e359a..cc18a8bb9 100644
--- a/helm/matita/library/nat/fermat_little_theorem.ma
+++ b/helm/matita/library/nat/fermat_little_theorem.ma
@@ -25,7 +25,7 @@ unfold S_mod.
 apply le_S_S_to_le.
 change with ((S i) \mod (S n) < S n).
 apply lt_mod_m_m.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 unfold injn.intros.
 apply inj_S.
 rewrite < (lt_to_eq_mod i (S n)).
@@ -37,14 +37,14 @@ elim Hcut1.
 (* i < n, j< n *)
 rewrite < mod_S.
 rewrite < mod_S.
-apply H2.simplify.apply le_S_S.apply le_O_n.
+apply H2.unfold lt.apply le_S_S.apply le_O_n.
 rewrite > lt_to_eq_mod.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite > lt_to_eq_mod.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
 (* i < n, j=n *)
 unfold S_mod in H2.
 simplify.
@@ -54,11 +54,11 @@ apply sym_eq.
 rewrite < (mod_n_n (S n)).
 rewrite < H4 in \vdash (? ? ? (? %?)).
 rewrite < mod_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite > lt_to_eq_mod.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
 (* i = n, j < n *)
 elim Hcut1.
 apply False_ind.
@@ -66,19 +66,19 @@ apply (not_eq_O_S (j \mod (S n))).
 rewrite < (mod_n_n (S n)).
 rewrite < H3 in \vdash (? ? (? %?) ?).
 rewrite < mod_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite > lt_to_eq_mod.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
 (* i = n, j= n*)
 rewrite > H3.
 rewrite > H4.
 reflexivity.
 apply le_to_or_lt_eq.assumption.
 apply le_to_or_lt_eq.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
 qed.
 
 (*
@@ -95,19 +95,19 @@ qed.
 
 theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
 n \lt p \to \not divides p n!.
-intros 3.elim n.simplify.intros.
+intros 3.elim n.unfold Not.intros.
 apply (lt_to_not_le (S O) p).
 unfold prime in H.elim H.
-assumption.apply divides_to_le.simplify.apply le_n.
+assumption.apply divides_to_le.unfold lt.apply le_n.
 assumption.
 change with (divides p ((S n1)*n1!) \to False).
 intro.
 cut (divides p (S n1) \lor divides p n1!).
 elim Hcut.apply (lt_to_not_le (S n1) p).
 assumption.
-apply divides_to_le.simplify.apply le_S_S.apply le_O_n.
+apply divides_to_le.unfold lt.apply le_S_S.apply le_O_n.
 assumption.apply H1.
-apply (trans_lt ? (S n1)).simplify. apply le_n.
+apply (trans_lt ? (S n1)).unfold lt. apply le_n.
 assumption.assumption.
 apply divides_times_to_divides.
 assumption.assumption.
@@ -120,19 +120,19 @@ split.intros.apply le_S_S_to_le.
 apply (trans_le ? p).
 change with (mod (a*i) p < p).
 apply lt_mod_m_m.
-simplify in H.elim H.
-simplify.apply (trans_le ? (S (S O))).
+unfold prime in H.elim H.
+unfold lt.apply (trans_le ? (S (S O))).
 apply le_n_Sn.assumption.
 rewrite < S_pred.apply le_n.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 unfold injn.intros.
 apply (nat_compare_elim i j).
 (* i < j *)
 intro.
 absurd (j-i \lt p).
-simplify.
+unfold lt.
 rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.
@@ -141,9 +141,9 @@ rewrite > sym_plus.
 apply le_plus_n.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 apply (le_to_not_lt p (j-i)).
-apply divides_to_le.simplify.
+apply divides_to_le.unfold lt.
 apply le_SO_minus.assumption.
 cut (divides p a \lor divides p (j-i)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.
@@ -152,7 +152,7 @@ rewrite > distr_times_minus.
 apply eq_mod_to_divides.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 apply sym_eq.
 apply H4.
 (* i = j *)
@@ -160,7 +160,7 @@ intro. assumption.
 (* j < i *)
 intro.
 absurd (i-j \lt p).
-simplify.
+unfold lt.
 rewrite > (S_pred p).
 apply le_S_S.
 apply le_plus_to_minus.
@@ -169,9 +169,9 @@ rewrite > sym_plus.
 apply le_plus_n.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 apply (le_to_not_lt p (i-j)).
-apply divides_to_le.simplify.
+apply divides_to_le.unfold lt.
 apply le_SO_minus.assumption.
 cut (divides p a \lor divides p (i-j)).
 elim Hcut.apply False_ind.apply H1.assumption.assumption.
@@ -180,7 +180,7 @@ rewrite > distr_times_minus.
 apply eq_mod_to_divides.
 unfold prime in H.
 elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
 apply H4.
 qed.
 
@@ -238,7 +238,7 @@ change with ((S O) \le pred p).
 apply le_S_S_to_le.rewrite < S_pred.
 unfold prime in H.elim H.assumption.assumption.
 unfold prime in H.elim H.apply (trans_lt ? (S O)).
-simplify.apply le_n.assumption.
+unfold lt.apply le_n.assumption.
 cut (O < a \lor O = a).
 elim Hcut.assumption.
 apply False_ind.apply H1.
diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index d42a57e8e..65f61b581 100644
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -136,7 +136,7 @@ intros.change with
 \land 
 gcd_aux (S m1) m (S m1) \divides (S m1)).
 apply divides_gcd_aux_mn.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 assumption.apply le_n.
 simplify.intro.
 apply (nat_case1 m).
@@ -152,8 +152,8 @@ cut (gcd_aux (S m1) n (S m1) \divides n
 gcd_aux (S m1) n (S m1) \divides S m1).
 elim Hcut.split.assumption.assumption.
 apply divides_gcd_aux_mn.
-simplify.apply le_S_S.apply le_O_n.
-apply not_lt_to_le.simplify.intro.apply H.
+unfold lt.apply le_S_S.apply le_O_n.
+apply not_lt_to_le.unfold Not. unfold lt.intro.apply H.
 rewrite > H1.apply (trans_le ? (S n)).
 apply le_n_Sn.assumption.apply le_n.
 qed.
@@ -221,13 +221,13 @@ apply (nat_case1 n).simplify.intros.assumption.
 intros.
 change with (d \divides gcd_aux (S m1) m (S m1)).
 apply divides_gcd_aux.
-simplify.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
+unfold lt.apply le_S_S.apply le_O_n.assumption.apply le_n.assumption.
 rewrite < H2.assumption.
 apply (nat_case1 m).simplify.intros.assumption.
 intros.
 change with (d \divides gcd_aux (S m1) n (S m1)).
 apply divides_gcd_aux.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 apply lt_to_le.apply not_le_to_lt.assumption.apply le_n.assumption.
 rewrite < H2.assumption.
 qed.
@@ -343,7 +343,7 @@ change with
 a*(S m1) - b*m = (gcd_aux (S m1) m (S m1)) 
 \lor b*m - a*(S m1) = (gcd_aux (S m1) m (S m1))).
 apply eq_minus_gcd_aux.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 assumption.apply le_n.
 apply (nat_case1 m).
 simplify.intros.
@@ -370,7 +370,7 @@ apply (ex_intro ? ? a1).
 apply (ex_intro ? ? a).
 left.assumption.
 apply eq_minus_gcd_aux.
-simplify. apply le_S_S.apply le_O_n.
+unfold lt. apply le_S_S.apply le_O_n.
 apply lt_to_le.apply not_le_to_lt.assumption.
 apply le_n.
 qed.
@@ -397,7 +397,7 @@ intros.
 generalize in match (gcd_O_to_eq_O m n H1).
 intros.elim H2.
 rewrite < H4 in \vdash (? ? %).assumption.
-intros.simplify.apply le_S_S.apply le_O_n.
+intros.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.
@@ -435,7 +435,7 @@ intro.
 apply divides_to_le.
 apply lt_O_gcd.
 rewrite > (times_n_O O).
-apply lt_times.simplify.apply le_S_S.apply le_O_n.assumption.
+apply lt_times.unfold lt.apply le_S_S.apply le_O_n.assumption.
 apply divides_d_gcd.
 apply (transitive_divides ? (S m1)).
 apply divides_gcd_m.
@@ -457,7 +457,7 @@ qed.
 
 theorem gcd_SO_n: \forall n:nat. gcd (S O) n = (S O).
 intro.
-apply antisym_le.apply divides_to_le.simplify.apply le_n.
+apply antisym_le.apply divides_to_le.unfold lt.apply le_n.
 apply divides_gcd_n.
 cut (O < gcd (S O) n \lor O = gcd (S O) n).
 elim Hcut.assumption.
@@ -502,7 +502,7 @@ qed.
 
 theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
 gcd n m = (S O).
-intros.simplify in H.change with (gcd n m = (S O)). 
+intros.unfold prime in H.change with (gcd n m = (S O)). 
 elim H.
 apply antisym_le.
 apply not_lt_to_le.
@@ -557,8 +557,8 @@ rewrite < (prime_to_gcd_SO n p).
 apply eq_minus_gcd.
 assumption.assumption.
 apply (decidable_divides n p).
-apply (trans_lt ? (S O)).simplify.apply le_n.
-simplify in H.elim H. assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.
+unfold prime in H.elim H. assumption.
 qed.
 
 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
@@ -576,11 +576,11 @@ rewrite < H2 in \vdash (? ? %).
 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 apply lt_SO_smallest_factor.assumption.
 apply divides_to_le.
-rewrite > H2.simplify.apply le_n.
+rewrite > H2.unfold lt.apply le_n.
 apply divides_d_gcd.assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 apply divides_gcd_n.
 apply (not_le_Sn_n (S O)).
 change with ((S O) < (S O)).
@@ -588,18 +588,18 @@ rewrite < H3 in \vdash (? ? %).
 apply (lt_to_le_to_lt ? (smallest_factor (gcd m (n*p)))).
 apply lt_SO_smallest_factor.assumption.
 apply divides_to_le.
-rewrite > H3.simplify.apply le_n.
+rewrite > H3.unfold lt.apply le_n.
 apply divides_d_gcd.assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
 apply divides_gcd_n.
 apply divides_times_to_divides.
 apply prime_smallest_factor_n.
 assumption.
 apply (transitive_divides ? (gcd m (n*p))).
 apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)).unfold lt. apply le_n. assumption.
 apply divides_gcd_m.
 change with (O < gcd m (n*p)).
 apply lt_O_gcd.
diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index 4897fb598..b8339f374 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -21,7 +21,7 @@ theorem monotonic_lt_plus_r:
 \forall n:nat.monotonic nat lt (\lambda m.n+m).
 simplify.intros.
 elim n.simplify.assumption.
-simplify.
+simplify.unfold lt.
 apply le_S_S.assumption.
 qed.
 
@@ -51,7 +51,7 @@ intro.elim n.
 rewrite > plus_n_O.
 rewrite > (plus_n_O q).assumption.
 apply H.
-simplify.apply le_S_S_to_le.
+unfold lt.apply le_S_S_to_le.
 rewrite > plus_n_Sm.
 rewrite > (plus_n_Sm q).
 exact H1.
@@ -65,7 +65,7 @@ qed.
 
 (* times and zero *)
 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
-intros.simplify.apply le_S_S.apply le_O_n.
+intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 (* times *)
@@ -172,7 +172,7 @@ rewrite < sym_times.
 rewrite < div_mod.
 rewrite > H2.
 assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
@@ -184,7 +184,7 @@ apply (lt_to_le_to_lt ? ((n / m)*m)).
 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
 rewrite < sym_times.
 rewrite > H2.
-simplify.
+simplify.unfold lt.
 rewrite < plus_n_O.
 rewrite < plus_n_Sm.
 apply le_S_S.
@@ -195,13 +195,13 @@ assumption.
 rewrite < sym_plus.
 apply le_plus_n.
 apply (trans_lt ? (S O)).
-simplify. apply le_n.assumption.
+unfold lt. apply le_n.assumption.
 qed.
 
 (* general properties of functions *)
 theorem monotonic_to_injective: \forall f:nat\to nat.
 monotonic nat lt f \to injective nat nat f.
-simplify.intros.
+unfold injective.intros.
 apply (nat_compare_elim x y).
 intro.apply False_ind.apply (not_le_Sn_n (f x)).
 rewrite > H1 in \vdash (? ? %).apply H.apply H2.
diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 00a90acd8..710418d72 100644
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -170,7 +170,7 @@ qed.
 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 intros.apply (lt_O_n_elim n H).intro.
 apply (lt_O_n_elim m H1).intro.
-simplify.apply le_S_S.apply le_minus_m.
+simplify.unfold lt.apply le_S_S.apply le_minus_m.
 qed.
 
 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
@@ -230,14 +230,14 @@ theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
 simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
-simplify.intros.
+simplify.intros.unfold lt.
 apply le_S_S.
 rewrite < plus_n_Sm.
 apply H.apply H1.
 qed.
 
 theorem distributive_times_minus: distributive nat times minus.
-simplify.
+unfold distributive.
 intros.
 apply ((leb_elim z y)).
   intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).
diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index fb7d1686e..a75032d71 100644
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -30,7 +30,7 @@ intros. reflexivity.
 qed.
 
 theorem injective_S : injective nat nat S.
-simplify.
+unfold injective.
 intros.
 rewrite > pred_Sn.
 rewrite > (pred_Sn y).
@@ -42,7 +42,7 @@ theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m
 
 theorem not_eq_S  : \forall n,m:nat. 
 \lnot n=m \to S n \neq S m.
-intros. simplify. intros.
+intros. unfold Not. intros.
 apply H. apply injective_S. assumption.
 qed.
 
@@ -53,7 +53,7 @@ definition not_zero : nat \to Prop \def
   | (S p) \Rightarrow True ].
 
 theorem not_eq_O_S : \forall n:nat. O \neq S n.
-intros. simplify. intros.
+intros. unfold Not. intros.
 cut (not_zero O).
 exact Hcut.
 rewrite > H.exact I.
@@ -91,7 +91,7 @@ intros.apply H2. apply H3.
 qed.
 
 theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
-intros.simplify.
+intros.unfold decidable.
 apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
 intro.elim n1.
 left.reflexivity.
diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 5fa636301..5330f52ad 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -45,10 +45,10 @@ apply not_le_to_lt.
 change with (smallest_factor (S n!) \le n \to False).intro.
 apply (not_divides_S_fact n (smallest_factor(S n!))).
 apply lt_SO_smallest_factor.
-simplify.apply le_S_S.apply le_SO_fact.
+unfold lt.apply le_S_S.apply le_SO_fact.
 assumption.
 apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
@@ -66,7 +66,7 @@ apply le_smallest_factor_n.
 apply prime_smallest_factor_n.
 change with ((S(S O)) \le S (S n1)!).
 apply le_S.apply le_SSO_fact.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
 qed.
 
 let rec nth_prime n \def
@@ -147,14 +147,14 @@ apply increasing_nth_prime.
 qed.
 
 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
-intros. elim n.simplify.apply le_n.
+intros. elim n.unfold lt.apply le_n.
 apply (trans_lt ? (nth_prime n1)).
 assumption.apply lt_nth_prime_n_nth_prime_Sn.
 qed.
 
 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
 intros.apply (trans_lt O (S O)).
-simplify. apply le_n.apply lt_SO_nth_prime_n.
+unfold lt. apply le_n.apply lt_SO_nth_prime_n.
 qed.
 
 theorem ex_m_le_n_nth_prime_m: 
@@ -195,6 +195,6 @@ apply (lt_nth_prime_to_not_prime a).assumption.assumption.
 apply (ex_intro nat ? a).assumption.
 apply le_to_or_lt_eq.assumption.
 apply ex_m_le_n_nth_prime_m.
-simplify.simplify in H.elim H.assumption.
+simplify.unfold prime in H.elim H.assumption.
 qed.
 
diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma
index b982accb3..24874c08a 100644
--- a/helm/matita/library/nat/ord.ma
+++ b/helm/matita/library/nat/ord.ma
@@ -167,7 +167,7 @@ generalize in match (H (n1 / m) m).
 elim (p_ord_aux n (n1 / m) m).
 apply H5.assumption.
 apply eq_mod_O_to_lt_O_div.
-apply (trans_lt ? (S O)).simplify.apply le_n.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.
 assumption.assumption.assumption.
 apply le_S_S_to_le.
 apply (trans_le ? n1).change with (n1 / m < n1).
@@ -175,9 +175,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
 change with (n1 \mod m \neq O).
 rewrite > H4.
-(* Andrea: META NOT FOUND !!!  
-rewrite > sym_eq. *)
-simplify.intro.
+unfold Not.intro.
 apply (not_eq_O_S m1).
 rewrite > H5.reflexivity.
 qed.
diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 0ddd4b5c5..6ec0c9992 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -54,7 +54,7 @@ interpretation "natural 'not greater than'" 'ngtr x y =
   (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
 
 theorem transitive_le : transitive nat le.
-simplify.intros.elim H1.
+unfold transitive.intros.elim H1.
 assumption.
 apply le_S.assumption.
 qed.
@@ -63,7 +63,7 @@ theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
 \def transitive_le.
 
 theorem transitive_lt: transitive nat lt.
-simplify.intros.elim H1.
+unfold transitive.unfold lt.intros.elim H1.
 apply le_S. assumption.
 apply le_S.assumption.
 qed.
@@ -105,11 +105,11 @@ qed.
 
 (* not le *)
 theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
-intros.simplify.intros.apply (leS_to_not_zero ? ? H).
+intros.unfold Not.simplify.intros.apply (leS_to_not_zero ? ? H).
 qed.
 
 theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
-intros.elim n.apply not_le_Sn_O.simplify.intros.cut (S n1 \leq n1).
+intros.elim n.apply not_le_Sn_O.unfold Not.simplify.intros.cut (S n1 \leq n1).
 apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.
@@ -119,19 +119,19 @@ theorem le_to_or_lt_eq : \forall n,m:nat.
 n \leq m \to n < m \lor n = m.
 intros.elim H.
 right.reflexivity.
-left.simplify.apply le_S_S.assumption.
+left.unfold lt.apply le_S_S.assumption.
 qed.
 
 (* not eq *)
 theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
-simplify.intros.cut ((le (S n) m) \to False).
+unfold Not.intros.cut ((le (S n) m) \to False).
 apply Hcut.assumption.rewrite < H1.
 apply not_le_Sn_n.
 qed.
 
 (* le vs. lt *)
 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
-simplify.intros.elim H.
+simplify.intros.unfold lt in H.elim H.
 apply le_S. apply le_n.
 apply le_S. assumption.
 qed.
@@ -145,13 +145,13 @@ theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
 intros 2.
 apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n)).
 intros.apply (absurd (O \leq n1)).apply le_O_n.assumption.
-simplify.intros.apply le_S_S.apply le_O_n.
-simplify.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.
+unfold Not.unfold lt.intros.apply le_S_S.apply le_O_n.
+unfold Not.unfold lt.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.
 assumption.
 qed.
 
 theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
-simplify.intros 3.elim H.
+unfold Not.unfold lt.intros 3.elim H.
 apply (not_le_Sn_n n H1).
 apply H2.apply lt_to_le. apply H3.
 qed.
@@ -165,7 +165,7 @@ qed.
 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
 intros.
 change with (Not (le (S m) n)).
-apply lt_to_not_le.simplify.
+apply lt_to_not_le.unfold lt.
 apply le_S_S.assumption.
 qed.
 
@@ -195,12 +195,12 @@ qed.
 (* lt and le trans *)
 theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
 intros.elim H1.
-assumption.simplify.apply le_S.assumption.
+assumption.unfold lt.apply le_S.assumption.
 qed.
 
 theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
 intros 4.elim H.
-assumption.apply H2.simplify.
+assumption.apply H2.unfold lt.
 apply lt_to_le.assumption.
 qed.
 
@@ -217,7 +217,7 @@ qed.
 
 (* other abstract properties *)
 theorem antisymmetric_le : antisymmetric nat le.
-simplify.intros 2.
+unfold antisymmetric.intros 2.
 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
 intros.apply le_n_O_to_eq.assumption.
 intros.apply False_ind.apply (not_le_Sn_O ? H).
@@ -232,11 +232,11 @@ theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
 theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
 intros.
 apply (nat_elim2 (\lambda n,m.decidable (n \leq m))).
-intros.simplify.left.apply le_O_n.
-intros.simplify.right.exact (not_le_Sn_O n1).
-intros 2.simplify.intro.elim H.
+intros.unfold decidable.left.apply le_O_n.
+intros.unfold decidable.right.exact (not_le_Sn_O n1).
+intros 2.unfold decidable.intro.elim H.
 left.apply le_S_S.assumption.
-right.intro.apply H1.apply le_S_S_to_le.assumption.
+right.unfold Not.intro.apply H1.apply le_S_S_to_le.assumption.
 qed.
 
 theorem decidable_lt: \forall n,m:nat. decidable (n < m).
@@ -265,7 +265,7 @@ definition increasing \def \lambda f:nat \to nat.
 
 theorem increasing_to_monotonic: \forall f:nat \to nat.
 increasing f \to monotonic nat lt f.
-simplify.intros.elim H1.apply H.
+unfold monotonic.unfold lt.unfold increasing.unfold lt.intros.elim H1.apply H.
 apply (trans_le ? (f n1)).
 assumption.apply (trans_le ? (S (f n1))).
 apply le_n_Sn.
@@ -278,7 +278,7 @@ intros.elim n.
 apply le_O_n.
 apply (trans_le ? (S (f n1))).
 apply le_S_S.apply H1.
-simplify in H. apply H.
+simplify in H. unfold increasing in H.unfold lt in H.apply H.
 qed.
 
 theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
@@ -289,7 +289,7 @@ elim H1.
 apply (ex_intro ? ? (S a)).
 apply (trans_le ? (S (f a))).
 apply le_S_S.assumption.
-simplify in H.
+simplify in H.unfold increasing in H.unfold lt in H.
 apply H.
 qed.
 
diff --git a/helm/matita/library/nat/permutation.ma b/helm/matita/library/nat/permutation.ma
index cc0f41027..3e987e9e8 100644
--- a/helm/matita/library/nat/permutation.ma
+++ b/helm/matita/library/nat/permutation.ma
@@ -22,7 +22,7 @@ definition injn: (nat \to nat) \to nat \to Prop \def
 i \le n \to j \le n \to f i = f j \to i = j.
 
 theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
-injn f (S n) \to injn f n.simplify.
+injn f (S n) \to injn f n.unfold injn.
 intros.apply H.
 apply le_S.assumption.
 apply le_S.assumption.
@@ -31,7 +31,7 @@ qed.
 
 theorem injective_to_injn: \forall f:nat \to nat. \forall n:nat.
 injective nat nat f \to injn f n.
-simplify.intros.apply H.assumption.
+unfold injective.unfold injn.intros.apply H.assumption.
 qed.
 
 definition permut : (nat \to nat) \to nat \to Prop 
@@ -199,9 +199,9 @@ simplify.
 rewrite > (not_eq_to_eqb_false k i).
 rewrite > (eqb_n_n k).
 simplify.reflexivity.
-simplify.intro.apply H1.apply sym_eq.assumption.
+unfold Not.intro.apply H1.apply sym_eq.assumption.
 assumption.
-simplify.intro.apply H2.apply (trans_eq ? ? n).
+unfold Not.intro.apply H2.apply (trans_eq ? ? n).
 apply sym_eq.assumption.assumption.
 intro.apply (eqb_elim n k).intro.
 simplify.
@@ -210,7 +210,7 @@ rewrite > (not_eq_to_eqb_false i j).
 simplify.
 rewrite > (eqb_n_n i).
 simplify.assumption.
-simplify.intro.apply H.apply sym_eq.assumption.
+unfold Not.intro.apply H.apply sym_eq.assumption.
 intro.simplify.
 rewrite > (not_eq_to_eqb_false n k H5).
 rewrite > (not_eq_to_eqb_false n j H4).
@@ -225,7 +225,7 @@ theorem permut_S_to_permut_transpose: \forall f:nat \to nat.
 (f n)) m.
 unfold permut.intros.
 elim H.
-split.intros.simplify.
+split.intros.simplify.unfold transpose.
 apply (eqb_elim (f i) (f (S m))).
 intro.apply False_ind.
 cut (i = (S m)).
@@ -310,7 +310,7 @@ qed.
 
 theorem bijn_transpose : \forall n,i,j. i \le n \to j \le n \to
 bijn (transpose i j) n.
-intros.simplify.intros.
+intros.unfold bijn.unfold transpose.intros.
 cut (m = i \lor \lnot m = i).
 elim Hcut.
 apply (ex_intro ? ? j).
@@ -354,7 +354,7 @@ qed.
 theorem permut_to_bijn: \forall n:nat.\forall f:nat\to nat.
 permut f n \to bijn f n.
 intro.
-elim n.simplify.intros.
+elim n.unfold bijn.intros.
 apply (ex_intro ? ? m).
 split.assumption.
 apply (le_n_O_elim m ? (\lambda p. f p = p)).
@@ -370,7 +370,7 @@ elim H1.apply H2.apply le_n.apply le_n.
 apply bijn_n_Sn.
 apply H.
 apply permut_S_to_permut_transpose.
-assumption.simplify.
+assumption.unfold transpose.
 rewrite > (eqb_n_n (f (S n1))).simplify.reflexivity.
 qed.
 
@@ -395,9 +395,9 @@ simplify.
 rewrite > (not_eq_to_eqb_false (f m) (f (S n1))).
 simplify.apply H2.
 apply injn_Sn_n. assumption.
-simplify.intro.absurd (m = S n1).
+unfold Not.intro.absurd (m = S n1).
 apply H3.apply le_S.assumption.apply le_n.assumption.
-simplify.intro.
+unfold Not.intro.
 apply (not_le_Sn_n n1).rewrite < H5.assumption.
 qed.
 
@@ -552,15 +552,15 @@ rewrite < H.
 rewrite < (H1 (g (S m + n))).
 apply eq_f.
 apply eq_map_iter_i.
-intros.unfold transpose.
+intros.simplify.unfold transpose.
 rewrite > (not_eq_to_eqb_false m1 (S m+n)).
 rewrite > (not_eq_to_eqb_false m1 (S (S m)+n)).
 simplify.
 reflexivity.
-apply (lt_to_not_eq m1 (S (S m)+n)).
-simplify.apply le_S_S.apply le_S.assumption.
+apply (lt_to_not_eq m1 (S ((S m)+n))).
+unfold lt.apply le_S_S.change with (m1 \leq S (m+n)).apply le_S.assumption.
 apply (lt_to_not_eq m1 (S m+n)).
-simplify.apply le_S_S.assumption.
+simplify.unfold lt.apply le_S_S.assumption.
 qed.
 
 theorem eq_map_iter_i_transpose_i_Si : \forall f:nat\to nat \to nat.associative nat f \to
@@ -579,11 +579,11 @@ apply eq_f2.unfold transpose.
 rewrite > (not_eq_to_eqb_false (S (S n1)+n) i).
 rewrite > (not_eq_to_eqb_false (S (S n1)+n) (S i)).
 simplify.reflexivity.
-simplify.intro.
+simplify.unfold Not.intro.
 apply (lt_to_not_eq i (S n1+n)).assumption.
 apply inj_S.apply sym_eq. assumption.
-simplify.intro.
-apply (lt_to_not_eq i (S (S n1+n))).simplify.
+simplify.unfold Not.intro.
+apply (lt_to_not_eq i (S (S n1+n))).simplify.unfold lt.
 apply le_S_S.assumption.
 apply sym_eq. assumption.
 apply H2.assumption.apply le_S_S_to_le.
@@ -608,13 +608,13 @@ exact H3.apply le_S_S_to_le.assumption.
 intros.
 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g (transpose i (S(m1 + i)) m)) f n)).
 apply H2.
-simplify. apply le_n.assumption.
+unfold lt. apply le_n.assumption.
 apply (trans_le ? (S(S (m1+i)))).
 apply le_S.apply le_n.assumption.
 apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g 
 (transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
 apply (H2 O ? ? (S(m1+i))).
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 apply (trans_le ? i).assumption.
 change with (i \le (S m1)+i).apply le_plus_n.
 exact H4.
@@ -623,23 +623,23 @@ apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
 (transpose (S(m1 + i)) (S(S(m1 + i))) 
 (transpose i (S(m1 + i)) m)))) f n)).
 apply (H2 m1).
-simplify. apply le_n.assumption.
+unfold lt. apply le_n.assumption.
 apply (trans_le ? (S(S (m1+i)))).
 apply le_S.apply le_n.assumption.
 apply eq_map_iter_i.
 intros.apply eq_f.
 apply sym_eq. apply eq_transpose.
-simplify. intro.
+unfold Not. intro.
 apply (not_le_Sn_n i).
 rewrite < H7 in \vdash (? ? %).
 apply le_S_S.apply le_S.
 apply le_plus_n.
-simplify. intro.
+unfold Not. intro.
 apply (not_le_Sn_n i).
 rewrite > H7 in \vdash (? ? %).
 apply le_S_S.
 apply le_plus_n.
-simplify. intro.
+unfold Not. intro.
 apply (not_eq_n_Sn (S m1+i)).
 apply sym_eq.assumption.
 qed.
@@ -726,11 +726,11 @@ rewrite > (not_eq_to_eqb_false (h m) (S n+n1)).
 simplify.apply H4.assumption.
 rewrite > H4.
 apply lt_to_not_eq.apply (trans_lt ? n1).assumption.
-simplify.apply le_S_S.apply le_plus_n.assumption.
+simplify.unfold lt.apply le_S_S.apply le_plus_n.assumption.
 unfold permut in H3.elim H3.
-simplify.intro.
+simplify.unfold Not.intro.
 apply (lt_to_not_eq m (S n+n1)).apply (trans_lt ? n1).assumption.
-simplify.apply le_S_S.apply le_plus_n.
+simplify.unfold lt.apply le_S_S.apply le_plus_n.
 unfold injn in H7.
 apply (H7 m (S n+n1)).apply (trans_le ? n1).
 apply lt_to_le.assumption.apply le_plus_n.apply le_n.
diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 8043d9a52..d595dad19 100644
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -43,7 +43,7 @@ simplify.rewrite > H.apply plus_n_Sm.
 qed.
 
 theorem associative_plus : associative nat plus.
-simplify.intros.elim x.
+unfold associative.intros.elim x.
 simplify.reflexivity.
 simplify.apply eq_f.assumption.
 qed.
diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index 452adc89c..50b7d1221 100644
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -27,7 +27,7 @@ interpretation "not divides" 'ndivides n m =
  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/primes/divides.ind#xpointer(1/1) n m)).
 
 theorem reflexive_divides : reflexive nat divides.
-simplify.
+unfold reflexive.
 intros.
 exact (witness x x (S O) (times_n_SO x)).
 qed.
@@ -151,7 +151,7 @@ apply (decidable_le n m).
 qed.
 
 theorem antisymmetric_divides: antisymmetric nat divides.
-simplify.intros.elim H. elim H1.
+unfold antisymmetric.intros.elim H. elim H1.
 apply (nat_case1 n2).intro.
 rewrite > H3.rewrite > H2.rewrite > H4.
 rewrite < times_n_O.reflexivity.
@@ -206,7 +206,7 @@ match eqb (m \mod n) O with
 | false \Rightarrow n \ndivides m].
 apply eqb_elim.
 intro.simplify.apply mod_O_to_divides.assumption.assumption.
-intro.simplify.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
+intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
 qed.
 
 theorem divides_b_true_to_divides :
@@ -339,11 +339,11 @@ definition prime : nat \to  Prop \def
 (\forall m:nat. m \divides n \to (S O) < m \to  m = n).
 
 theorem not_prime_O: \lnot (prime O).
-simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
+unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
 qed.
 
 theorem not_prime_SO: \lnot (prime (S O)).
-simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
+unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 qed.
 
 (* smallest factor *)
@@ -390,10 +390,10 @@ theorem lt_O_smallest_factor: \forall n:nat. O < n \to O < (smallest_factor n).
 intro.
 apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_n O H).
 intro.apply (nat_case m).intro.
-simplify.apply le_n.
+simplify.unfold lt.apply le_n.
 intros.apply (trans_lt ? (S O)).
-simplify. apply le_n.
-apply lt_SO_smallest_factor.simplify. apply le_S_S.
+unfold lt.apply le_n.
+apply lt_SO_smallest_factor.unfold lt. apply le_S_S.
 apply le_S_S.apply le_O_n.
 qed.
 
@@ -414,7 +414,7 @@ apply (ex_intro nat ? (S(S m1))).
 split.split.
 apply le_minus_m.apply le_n.
 rewrite > mod_n_n.reflexivity.
-apply (trans_lt ? (S O)).apply (le_n (S O)).simplify.
+apply (trans_lt ? (S O)).apply (le_n (S O)).unfold lt.
 apply le_S_S.apply le_S_S.apply le_O_n.
 qed.
   
@@ -423,9 +423,9 @@ theorem le_smallest_factor_n :
 intro.apply (nat_case n).simplify.reflexivity.
 intro.apply (nat_case m).simplify.reflexivity.
 intro.apply divides_to_le.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem lt_smallest_factor_to_not_divides: \forall n,i:nat. 
@@ -459,7 +459,7 @@ absurd (m \divides n).
 apply (transitive_divides m (smallest_factor n)).
 assumption.
 apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). simplify. apply le_n. exact H.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. exact H.
 apply lt_smallest_factor_to_not_divides.
 exact H.assumption.assumption.assumption.
 apply divides_to_le.
@@ -481,7 +481,7 @@ change with
 smallest_factor (S(S m1)) = (S(S m1))).
 intro.elim H.apply H2.
 apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)).simplify. apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt. apply le_n.assumption.
 apply lt_SO_smallest_factor.
 assumption.
 qed.
@@ -517,8 +517,8 @@ match primeb n with
 [ true \Rightarrow prime n
 | false \Rightarrow \lnot (prime n)].
 intro.
-apply (nat_case n).simplify.intro.elim H.apply (not_le_Sn_O (S O) H1).
-intro.apply (nat_case m).simplify.intro.elim H.apply (not_le_Sn_n (S O) H1).
+apply (nat_case n).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_O (S O) H1).
+intro.apply (nat_case m).simplify.unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 intro.
 change with 
 match eqb (smallest_factor (S(S m1))) (S(S m1)) with
@@ -528,7 +528,7 @@ apply (eqb_elim (smallest_factor (S(S m1))) (S(S m1))).
 intro.change with (prime (S(S m1))).
 rewrite < H.
 apply prime_smallest_factor_n.
-simplify.apply le_S_S.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_S_S.apply le_O_n.
 intro.change with (\lnot (prime (S(S m1)))).
 change with (prime (S(S m1)) \to False).
 intro.apply H.
diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index 70a4fd76e..2ae5ffd74 100644
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -52,7 +52,7 @@ reflexivity.
 qed.
 
 theorem symmetric_times : symmetric nat times. 
-simplify.
+unfold symmetric.
 intros.elim x.
 simplify.apply times_n_O.
 simplify.rewrite > H.apply times_n_Sm.
@@ -62,7 +62,7 @@ variant sym_times : \forall n,m:nat. n*m = m*n \def
 symmetric_times.
 
 theorem distributive_times_plus : distributive nat times plus.
-simplify.
+unfold distributive.
 intros.elim x.
 simplify.reflexivity.
 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
@@ -74,7 +74,7 @@ variant distr_times_plus: \forall n,m,p:nat. n*(m+p) = n*m + n*p
 \def distributive_times_plus.
 
 theorem associative_times: associative nat times.
-simplify.intros.
+unfold associative.intros.
 elim x.simplify.apply refl_eq.
 simplify.rewrite < sym_times.
 rewrite > distr_times_plus.
diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma
index ff425772c..24c3920ed 100644
--- a/helm/matita/library/nat/totient.ma
+++ b/helm/matita/library/nat/totient.ma
@@ -68,35 +68,35 @@ rewrite < H4.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < H5.
 rewrite > sym_gcd.
 rewrite > gcd_mod.
 apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite > sym_times.
 assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 intro.
 apply eqb_elim.
 intro.apply eqb_elim.
 intro.apply False_ind.
 apply H6.
 apply eq_gcd_times_SO.
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < gcd_mod.
 rewrite > H4.
 rewrite > sym_gcd.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 rewrite < gcd_mod.
 rewrite > H5.
 rewrite > sym_gcd.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 intro.reflexivity.
 intro.reflexivity.
 qed.
\ No newline at end of file
diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
index 75a1693f4..1001d2351 100644
--- a/helm/matita/tests/simpl.ma
+++ b/helm/matita/tests/simpl.ma
@@ -28,7 +28,7 @@ theorem a :
  \forall x,y : A.
  not (x = y) \to not(y = x).
 intros.
-simplify.
+unfold not. (* simplify. *)
 intro. apply H.
 symmetry.
 exact H1.