Yet another semantics for simplify.

[helm.git] / helm / matita / library / list / sort.ma

diff --git a/helm/matita/library/list/sort.ma b/helm/matita/library/list/sort.ma
index 2d60662a4d8f19e3d3d5894110782878a9927092..1cc127759f0b37f8778491389718224a0215a85f 100644 (file)
--- 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);