From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 16 Apr 2007 21:16:11 +0000 (+0000)
Subject: better simplify
X-Git-Tag: 0.4.95@7852~531
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7c84225a8e472e754f1baf8f8b37f8627c8da6fa;p=helm.git

better simplify
---

diff --git a/matita/library/decidable_kit/eqtype.ma b/matita/library/decidable_kit/eqtype.ma
index 7b0f94ed4..97fdf8907 100644
--- a/matita/library/decidable_kit/eqtype.ma
+++ b/matita/library/decidable_kit/eqtype.ma
@@ -138,20 +138,18 @@ generalize in match (refl_eq ? (ocmp ? a b));
 generalize in match (ocmp ? a b) in ⊢ (? ? ? % → %); intros 1 (c);
 cases c; intros (H); [ apply reflect_true | apply reflect_false ];
 generalize in match H; clear H;
-cases a; cases b;
-[1: intros; reflexivity;
-|2,3: intros (H); destruct H;
-|4: intros (H); simplify in H; rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity; 
-    (* se faccio la rewrite diretta non tipa *)
-|5: intros (H H1); destruct H
-|6,7: unfold Not; intros (H H1); destruct H1
-|8: unfold Not; simplify; intros (H H1); 
+cases a; cases b; simplify; intros (H);
+[1: reflexivity;
+|2,3,5: destruct H;
+|4: rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity; 
+|6,7: unfold Not; intros (H1); destruct H1
+|8: unfold Not; intros (H1); 
     (* ancora injection non va *)
     cut (s = s1); [ rewrite > Hcut in H;  rewrite > cmp_refl in H;  destruct H;].
     change with (match (Some d s) with
                  [ None ⇒ s | (Some s) ⇒ s] = s1); rewrite > H1;
-                 simplify; reflexivity;
-] qed.
+                 simplify; reflexivity;] 
+qed.
 
 definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d).
 definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝
diff --git a/matita/library/decidable_kit/fintype.ma b/matita/library/decidable_kit/fintype.ma
index bb3553b00..ffd41d206 100644
--- a/matita/library/decidable_kit/fintype.ma
+++ b/matita/library/decidable_kit/fintype.ma
@@ -38,12 +38,11 @@ definition segment_enum  ≝
   λbound.filter ? ? (if_p nat_eqType (λx.ltb x bound)) (iota O bound).
 
 lemma iota_ltb : ∀x,p:nat. mem nat_eqType x (iota O p) = ltb x p.
-intros (x p); elim p; simplify; [1:reflexivity]
-rewrite < leb_eqb;
+intros (x p); elim p; simplify;[reflexivity] 
 generalize in match (refl_eq ? (cmp ? x n));
-generalize in match (cmp ? x n) in ⊢ (? ? % ? → %); intros 1 (b);
-cases b; simplify; intros (H1); [1: reflexivity]
-rewrite > H; fold simplify (ltb x n); rewrite > H1; reflexivity;
+generalize in match (cmp ? x n) in ⊢ (? ? ? % → %); intros 1 (b);
+cases b; simplify; intros (H1); rewrite > H; clear H;
+rewrite < (leb_eqb x n); rewrite > H1; reflexivity;
 qed.
 
 lemma mem_filter :
@@ -52,29 +51,29 @@ lemma mem_filter :
     match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) →
   mem d2 x (filter d1 d2 p l) = false.
 intros 5 (d1 d2 x l p); 
-elim l; [1: simplify; auto]
-simplify; fold simplify (filter d1 d2 p l1);
+elim l; simplify; [reflexivity]
 generalize in match (refl_eq ? (p t));
-generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-[1: simplify; intros (Hpt); apply H; intros (y Hyl);
-  apply H1; simplify; fold simplify (orb (cmp ? y t) (mem ? y l1));
-  rewrite > Hyl; rewrite > orbC; reflexivity;
-|2:simplify; intros (Hpt); 
-  generalize in match (refl_eq ? (cmp ? x s));
-  generalize in match (cmp ? x s) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-  [1: simplify; intros (Exs);
-      rewrite < (H1 t); [2: simplify; rewrite > cmp_refl; reflexivity;]
-      rewrite > Hpt; simplify; symmetry; assumption;
-  |2: intros (Dxs); simplify; apply H; intros;
-      apply H1; simplify; fold simplify (orb (cmp ? y t) (mem ? y l1));
-      rewrite > H2; rewrite > orbC; reflexivity;]]
+generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (Hpt);
+[1: apply H; intros (y Hyl);
+    apply H1; simplify; 
+    rewrite > Hyl; rewrite > orbC; reflexivity;
+|2: generalize in match (refl_eq ? (cmp ? x s));
+    generalize in match (cmp ? x s) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
+    [1: simplify; intros (Exs);
+        rewrite > orbC; rewrite > H;
+        [2: intros; apply H1; simplify; rewrite > H2; rewrite > orbC; reflexivity
+        |1: lapply (H1 t) as H2; [2: simplify; rewrite > cmp_refl; reflexivity]
+            rewrite > Hpt in H2; simplify in H2; rewrite > H2 in Exs;
+            destruct Exs;] 
+    |2: intros (Dxs); simplify; rewrite > H;
+        [2: intros; apply (H1 y); simplify; rewrite > H2; rewrite > orbC; reflexivity
+        |1: rewrite > Dxs; reflexivity]]]
 qed.
   
 lemma count_O : 
   ∀d:eqType.∀p:d→bool.∀l:list d. 
     (∀x:d.mem d x l = true → notb (p x) = true) → count d p l = O.
 intros 3 (d p l); elim l; simplify; [1: reflexivity]
-fold simplify (count d p l1); (* XXX simplify troppo *)
 generalize in match (refl_eq ? (p t));
 generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b);
 cases b; simplify; 
@@ -96,65 +95,49 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
    generalize in match Hn; generalize in match Hn; clear Hn;
    unfold segment_enum;
    generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
-   intros 1 (m); elim m  (Hm Hn p IH Hm Hn);
-   [ destruct Hm;
-   | simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
-     (* XXX simplify che spacca troppo *)
-     fold simplify (filter nat_eqType (sigma nat_eqType (λx.ltb x bound))
-                     (if_p nat_eqType (λx.ltb x bound)) (iota O p));
-     [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?);
-        unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
-        simplify in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
-        generalize in match (refl_eq ? (eqb n p));
-        generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b);
-        cases b; simplify;
-        [2:intros (Enp); rewrite > IH; [1,3: auto]
-           rewrite <  ltb_n_Sm in Hm; rewrite > Enp in Hm;
-           generalize in match Hm; cases (ltb n p); intros; [1:reflexivity]
-           simplify in H1; destruct H1;
-        |1:clear IH; intros (Enp); 
-           fold simplify (count fsort (cmp fsort {n, Hn})
-                           (filter ? (sigma nat_eqType (λx.ltb x bound))
-                           (if_p nat_eqType (λx.ltb x bound)) (iota O p)));
-           rewrite > (count_O fsort); [1: reflexivity]
-           intros 1 (x); 
-           rewrite < (b2pT ? ? (eqP ? n ?) Enp);
-           cases x (y Hy); intros (ABS); clear x;
-           unfold segment; unfold notb; simplify; 
-           generalize in match (refl_eq ? (cmp ? n y));
-           generalize in match (cmp ? n y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-           intros (Eny); simplify; [2: auto]
-           rewrite < ABS; symmetry; clear ABS;
-           generalize in match Hy; clear Hy; rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny);
-           simplify; intros (Hn); fold simplify (iota O n);
-           apply (mem_filter nat_eqType fsort);
-           intros (w Hw);
-           fold simplify (sort nat_eqType);
-           cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
-           simplify; [2: reflexivity]
-           generalize in match H1; clear H1; cases s; clear s; intros (H1);
-           unfold segment; simplify; simplify in H1; rewrite > H1;
-           rewrite > iota_ltb in Hw;
-           apply (p2bF ? ? (eqP nat_eqType ? ?));
-           unfold Not; intros (Enw);
-           rewrite > Enw in Hw; rewrite > ltb_refl in Hw; destruct Hw]
-     |2:rewrite > IH; [1:reflexivity|3:assumption]
-          rewrite <  ltb_n_Sm in Hm;
-          cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption]
-          rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn;
-          rewrite > Hn in H; cases (H ?); reflexivity;
-     ]]]      
+   intros 1 (m); elim m  (Hm Hn p IH Hm Hn); [ destruct Hm ]
+   simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
+   [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?);
+      unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
+      simplify;
+      generalize in match (refl_eq ? (eqb n p));
+      generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b); cases b; clear b; 
+      intros (Enp); simplify;
+      [2:rewrite > IH; [1,3: auto]
+         rewrite <  ltb_n_Sm in Hm; rewrite > Enp in Hm;
+         generalize in match Hm; cases (ltb n p); intros; [reflexivity]
+         simplify in H1; destruct H1;
+      |1:clear IH; rewrite > (count_O fsort); [reflexivity]
+         intros 1 (x); rewrite < (b2pT ? ? (eqP ? n ?) Enp);
+         cases x (y Hy); intros (ABS); clear x;
+         unfold segment; unfold notb; simplify; 
+         generalize in match (refl_eq ? (cmp ? n y));
+         generalize in match (cmp ? n y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
+         intros (Eny); simplify; [2:reflexivity]
+         rewrite < ABS; symmetry; clear ABS;
+         generalize in match Hy; clear Hy; 
+         rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny);
+         simplify; intros (Hn); apply (mem_filter nat_eqType fsort); intros (w Hw);
+         fold simplify (sort nat_eqType); (* CANONICAL?! *)
+         cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
+         simplify; [2: reflexivity]
+         generalize in match H1; clear H1; cases s; clear s; intros (H1);
+         unfold segment; simplify; simplify in H1; rewrite > H1;
+         rewrite > iota_ltb in Hw; apply (p2bF ? ? (eqP nat_eqType ? ?));
+         unfold Not; intros (Enw); rewrite > Enw in Hw; 
+         rewrite > ltb_refl in Hw; destruct Hw]
+   |2:rewrite > IH; [1:reflexivity|3:assumption]
+      rewrite <  ltb_n_Sm in Hm;
+      cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption]
+      rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn;
+      rewrite > Hn in H; cases (H ?); reflexivity]]
 qed.
 
 let rec uniq (d:eqType) (l:list d) on l : bool ≝
   match l with 
-  [ nil⇒ true 
+  [ nil ⇒ true 
   | (cons x tl) ⇒ andb (notb (mem d x tl)) (uniq d tl)].
 
-lemma uniq_tail_OLD : ∀d:eqType.∀x:d.∀l:list d.uniq d (x::l) = true → uniq d l = true.
-intros (d x l Uxl); simplify in Uxl; cases (b2pT ? ? (andbP ? ?) Uxl); assumption;
-qed.
-
 lemma uniq_mem : ∀d:eqType.∀x:d.∀l:list d.uniq d (x::l) = true → mem d x l = false.
 intros (d x l H); simplify in H; lapply (b2pT ? ? (andbP ? ?) H) as H1; clear H;
 cases H1 (H2 H3); lapply (b2pT ? ?(negbP ?) H2); assumption;
@@ -168,74 +151,59 @@ intros; cases a; cases b; reflexivity; qed.
 
 lemma uniq_tail : 
   ∀d:eqType.∀x:d.∀l:list d. uniq d (x::l) = andb (negb (mem d x l)) (uniq d l).
-intros (d x l);
-elim l; [1: simplify; reflexivity]
+intros (d x l); elim l; simplify; [reflexivity]
 generalize in match (refl_eq ? (cmp d x t));
 generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-intros (E); simplify ; rewrite > E; simplify; [1: reflexivity;]
+intros (E); simplify ; rewrite > E; [reflexivity]
 rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
-rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA;
-reflexivity;
+rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
 qed.
   
 lemma count_O_mem : ∀d:eqType.∀x:d.∀l:list d.ltb O (count d (cmp d x) l) = mem d x l.
-intros 3 (d x l); elim l [reflexivity]
-simplify; fold simplify (mem d x l1); fold simplify (count d (cmp d x) l1);
-rewrite < H; cases (cmp d x t); simplify; reflexivity;
-qed.
+intros 3 (d x l); elim l [reflexivity] simplify; rewrite < H; cases (cmp d x t);
+reflexivity; qed.
   
 lemma uniqP : ∀d:eqType.∀l:list d. 
   reflect (∀x:d.mem d x l = true → count d (cmp d x) l = (S O)) (uniq d l).
 intros (d l); apply prove_reflect; elim l; [1: destruct H1 | 3: destruct H]
-[1: generalize in match H2; simplify in H2; fold simplify (orb (cmp d x t) (mem d x l1)) in H2;
-    (* lapply (uniq_tail ? ? ? H1) as Ul1; *) 
+[1: generalize in match H2; simplify in H2; 
     lapply (b2pT ? ? (orbP ? ?) H2) as H3; clear H2; 
     cases H3; clear H3; intros;
     [2: lapply (uniq_mem ? ? ? H1) as H4; 
         generalize in match (refl_eq ? (cmp d x t));
         generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
         intros (H5);
-        [1: simplify; rewrite > H5; simplify; fold simplify (count d (cmp d x) l1);
-            rewrite > count_O; [1:reflexivity]
+        [1: simplify; rewrite > H5; simplify; rewrite > count_O; [reflexivity]
             intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H5) in H2 H3 H4 ⊢ %;
             clear H5; clear x; rewrite > H2 in H4; destruct H4;
-         |2: simplify; rewrite > H5; simplify;
-             fold simplify (count d (cmp d x) (l1));
-             apply H; rewrite > uniq_tail in H1;
-             cases (b2pT ? ? (andbP ? ?) H1);
+         |2: simplify; rewrite > H5; simplify; apply H; 
+             rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); 
              assumption;]
-    |1: simplify; rewrite > H2; simplify;
-        fold simplify (count d (cmp d x) l1);
-        rewrite > count_O; [1:reflexivity]
+    |1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]
         intros (y Hy); rewrite > (b2pT ? ? (eqP d ? ?) H2) in H3 ⊢ %;
-        clear H2; clear x;
-        lapply (uniq_mem ? ? ? H1) as H4;
+        clear H2; clear x; lapply (uniq_mem ? ? ? H1) as H4;
         generalize in match (refl_eq ? (cmp d t y));
-        generalize in match (cmp d t y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-        [1: intros (E); rewrite > (b2pT ? ? (eqP d ? ?) E) in H4;
+        generalize in match (cmp d t y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b; intros (E);
+        [1: rewrite > (b2pT ? ? (eqP d ? ?) E) in H4;
             rewrite > H4 in Hy; destruct Hy;
         |2:intros; reflexivity]]
 |2: rewrite > uniq_tail in H1;
     generalize in match (refl_eq ? (uniq d l1));
     generalize in match (uniq d l1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
     [1: intros (E); rewrite > E in H1; rewrite > andbC in H1; simplify in H1;
-      unfold Not; intros (A); lapply (A t) as A'; 
-      [1: simplify in A'; 
-          rewrite > cmp_refl in A'; simplify in A';
-          destruct A'; clear A'; fold simplify (count d (cmp d t) l1) in Hcut;
-          rewrite < count_O_mem in H1;
-          rewrite > Hcut in H1; destruct H1;  
-      |2: simplify; rewrite > cmp_refl; reflexivity;]
+        unfold Not; intros (A); lapply (A t) as A'; 
+        [1: simplify in A'; rewrite > cmp_refl in A'; simplify in A';
+            destruct A'; clear A'; rewrite < count_O_mem in H1;
+            rewrite > Hcut in H1; destruct H1;  
+        |2: simplify; rewrite > cmp_refl; reflexivity;]
     |2: intros (Ul1); lapply (H Ul1); unfold Not; intros (A); apply Hletin;
-        intros (r Mrl1); lapply (A r); [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity]   
+        intros (r Mrl1); lapply (A r); 
+          [2: simplify; rewrite > Mrl1; cases (cmp d r t); reflexivity]   
         generalize in match (refl_eq ? (cmp d r t));
         generalize in match (cmp d r t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
         [1: intros (E); simplify in Hletin1; rewrite > E in Hletin1;
-            simplify in Hletin1; fold simplify (count d (cmp d r) l1) in Hletin1;
-            destruct Hletin1;
-            rewrite < count_O_mem in Mrl1;
-            rewrite > Hcut in Mrl1;
-            destruct Mrl1;
+            destruct Hletin1; rewrite < count_O_mem in Mrl1;
+            rewrite > Hcut in Mrl1; destruct Mrl1;
         |2: intros; simplify in Hletin1; rewrite > H2 in Hletin1;
             simplify in Hletin1; apply (Hletin1);]]]
 qed.
@@ -254,46 +222,42 @@ lemma sub_enumP : ∀d:finType.∀p:d→bool.∀x:sub_eqType d p.
 intros (d p x); cases x (t Ht); clear x;
 generalize in match (mem_finType d t); 
 generalize in match (uniq_fintype_enum d); 
-elim (enum d); [1:destruct H1]
-simplify; fold simplify (filter d (sigma d p) (if_p d p) l); 
-cases (in_sub_eq d p t1); simplify in ⊢ (? ? (? ? ? %) ?); 
- [simplify; fold simplify (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht})
-                        (filter d (sigma d p) (if_p d p) l));
-  generalize in match H3; clear H3; cases s (r Hr); clear s;
-  simplify; intros (Ert1); generalize in match Hr; clear Hr;
-  rewrite > Ert1; clear Ert1; clear r; intros (Ht1);
-  unfold  sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?); 
-  simplify; generalize in match (refl_eq ? (cmp d t t1));
-  generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-  intros (Ett1); simplify; 
-    [1: cut (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht})
+elim (enum d); [destruct H1] simplify;  
+cases (in_sub_eq d p t1); simplify; 
+[1:generalize in match H3; clear H3; cases s (r Hr); clear s;
+   simplify; intros (Ert1); generalize in match Hr; clear Hr;
+   rewrite > Ert1; clear Ert1; clear r; intros (Ht1);
+   unfold  sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?); 
+   simplify; generalize in match (refl_eq ? (cmp d t t1));
+   generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
+   intros (Ett1); simplify; 
+   [1: cut (count (sub_eqType d p) (cmp (sub_eqType d p) {t,Ht})
             (filter d (sigma d p) (if_p d p) l) = O); [1:rewrite > Hcut; reflexivity]
-        lapply (uniq_mem ? ? ? H1);
-        generalize in match Ht; 
-        rewrite > (b2pT ? ? (eqP d ? ?) Ett1); intros (Ht1'); clear Ht1;
-        generalize in match Hletin; elim l; [1: reflexivity]
-        simplify; cases (in_sub_eq d p t2); simplify; 
-          [1: generalize in match H5; cases s; simplify; intros; clear H5; 
-              unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
-              simplify; rewrite > H7; simplify in H4;
-              generalize in match H4; clear H4; 
-              generalize in match (refl_eq ? (cmp d t1 t2));
-              generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-              simplify; intros; [1: destruct H5] apply H3; assumption
-          |2:apply H3;
-              generalize in match H4; clear H4; simplify;
-              generalize in match (refl_eq ? (cmp d t1 t2));
-              generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-              simplify; intros; [1: destruct H6] assumption;]
-    |2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
-        simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption] 
- | rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
+       lapply (uniq_mem ? ? ? H1);
+       generalize in match Ht; 
+       rewrite > (b2pT ? ? (eqP d ? ?) Ett1); intros (Ht1'); clear Ht1;
+       generalize in match Hletin; elim l; [ reflexivity]
+       simplify; cases (in_sub_eq d p t2); simplify; 
+       [1: generalize in match H5; cases s; simplify; intros; clear H5; 
+           unfold sub_eqType in ⊢ (? ? match ? (% ? ?) ? ? with [true⇒ ?|false⇒ ?] ?);
+           simplify; rewrite > H7; simplify in H4;
+           generalize in match H4; clear H4; 
+           generalize in match (refl_eq ? (cmp d t1 t2));
+           generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
+           simplify; intros; [1: destruct H5] apply H3; assumption;
+       |2: apply H3;
+           generalize in match H4; clear H4; simplify;
+           generalize in match (refl_eq ? (cmp d t1 t2));
+           generalize in match (cmp d t1 t2) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
+           simplify; intros; [1: destruct H6] assumption;]
+   |2: apply H; [ rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
+       simplify in H2; rewrite > Ett1 in H2; simplify in H2; assumption] 
+|2:rewrite > H; [1:reflexivity|2: rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); assumption]
    simplify in H2; generalize in match H2; generalize in match (refl_eq ? (cmp d t t1));
    generalize in match (cmp d t t1) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
-   intros (E); 
-     [lapply (b2pT ? ? (eqP d ? ?) E); clear H; rewrite > Hletin in Ht;
-      rewrite > Ht in H3; destruct H3;
-     |assumption]]
+   intros (E); [2:assumption] 
+   lapply (b2pT ? ? (eqP d ? ?) E); clear H; rewrite > Hletin in Ht;
+   rewrite > Ht in H3; destruct H3;]
 qed.
  
 definition sub_finType : ∀d:finType.∀p:d→bool.finType ≝
diff --git a/matita/library/decidable_kit/list_aux.ma b/matita/library/decidable_kit/list_aux.ma
index 8f30d3f6f..d641d9018 100644
--- a/matita/library/decidable_kit/list_aux.ma
+++ b/matita/library/decidable_kit/list_aux.ma
@@ -32,8 +32,7 @@ definition count : ∀T : eqType.∀f : T → bool.∀l : list T. nat :=
 let rec mem (d : eqType) (x : d) (l : list d) on l : bool ≝
   match l with
   [ nil ⇒ false 
-  | cons y tl ⇒
-     match (cmp d x y) with [ true ⇒ true | false ⇒ mem d x tl]].
+  | cons y tl ⇒ orb (cmp d x y) (mem d x tl)].
 
 definition iota : nat → nat → list nat ≝
   λn,m. nat_rect (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
@@ -49,17 +48,12 @@ lemma list_ind2 :
   (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → 
   P l1 l2.
 intros (T1 T2 l1 l2 P Hl Pnil Pcons);
-generalize in match Hl; clear Hl;
-generalize in match l2; clear l2;
-elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| destruct Hl]
-| intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl] 
-  intros 1 (Hl); apply Pcons;
-  apply IH; destruct Hl; 
-  (* XXX simplify in Hl non folda length *) 
-  assumption;]
+generalize in match Hl; clear Hl; generalize in match l2; clear l2;
+elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| destruct Hl]]
+intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl] 
+intros 1 (Hl); apply Pcons; apply IH; destruct Hl; assumption;
 qed.
-  
- 
+
 lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
 intros (A B f g l Efg); elim l; simplify; [1: reflexivity ];
 rewrite > (Efg t); rewrite > H; reflexivity;  
@@ -76,13 +70,12 @@ lemma lcmp_length :
   ∀d:eqType.∀l1,l2:list d.
  lcmp ? l1 l2 = true → length ? l1 = length ? l2.
 intros 2 (d l1); elim l1 1 (l2 x1);
-[ cases l2; simplify; intros;[reflexivity|destruct H] 
-| intros 3 (tl1 IH l2); cases (l2); intros; [1:destruct H]
-  simplify; (* XXX la apply non fa simplify? *) 
-  apply congr_S; apply (IH l);
-  (* XXX qualcosa di enorme e' rotto! la regola di convertibilita?! *)
-  simplify in H;
-  letin H' ≝ (b2pT ? ? (andbP ? ?) H); decompose; assumption]
+[1: cases l2; simplify; intros; [reflexivity|destruct H] 
+|2: intros 3 (tl1 IH l2); cases (l2); intros; [1:destruct H]
+    simplify; (* XXX la apply non fa simplify? *) 
+    apply congr_S; apply (IH l);
+    (* XXX qualcosa di enorme e' rotto! la regola di convertibilita?! *)
+    simplify in H; cases (b2pT ? ? (andbP ? ?) H); assumption]
 qed.
 
 lemma lcmpP : ∀d:eqType.∀l1,l2:list d. eq_compatible (list d) l1 l2 (lcmp d l1 l2).
@@ -90,34 +83,27 @@ intros (d l1 l2);
 generalize in match (refl_eq ? (lcmp d l1 l2));
 generalize in match (lcmp d l1 l2) in ⊢ (? ? ? % → %); intros 1 (c);
 cases c; intros (H); [ apply reflect_true | apply reflect_false ]
-[ letin Hl≝ (lcmp_length ? ? ? H); clearbody Hl;
+[ lapply (lcmp_length ? ? ? H) as Hl;
   generalize in match H; clear H;
   apply (list_ind2 ? ? ? ? ? Hl); [1: intros; reflexivity]
-  simplify; intros (tl1 tl2 hd1 hd2 IH H);
-  letin H' ≝ (b2pT ? ? (andbP ? ?) H); decompose;
+  simplify; intros (tl1 tl2 hd1 hd2 IH H); cases (b2pT ? ? (andbP ? ?) H);
   rewrite > (IH H2); rewrite > (b2pT ? ? (eqP d ? ?) H1); reflexivity
 | generalize in match H; clear H; generalize in match l2; clear l2;
   elim l1 1 (l1 x1);
-   [ cases l1; [intros; destruct H]
-     unfold Not; intros; destruct H1;
+   [ cases l1; [intros; destruct H | unfold Not; intros; destruct H1;]
    | intros 3 (tl1 IH l2); cases l2;
      [ unfold Not; intros; destruct H1;
      | simplify;  intros;
-       letin H' ≝ (p2bT ? ? (negbP ?) H); clearbody H'; clear H;
-       letin H'' ≝ (b2pT ? ? (andbPF ? ?) H'); clearbody H''; clear H';
-       cases H''; clear H'';
-       [ intros; 
-         letin H' ≝ (b2pF ? ? (eqP d ? ?) H); clearbody H'; clear H;
-         (* XXX destruct H1; *)
+       cases (b2pT ? ? (andbPF ? ?) (p2bT ? ? (negbP ?) H)); clear H;
+       [ intros; lapply (b2pF ? ? (eqP d ? ?) H1) as H'; clear H1;
+         (* XXX destruct H; *)
          change in H' with (Not ((match (x1::tl1) with [nil⇒x1|(cons x1 _) ⇒ x1]) = s));
-         rewrite > H1 in H'; simplify in H'; apply H'; reflexivity;
-       | intros; 
-         letin H' ≝ (IH ? H); clearbody H';
+         rewrite > H in H'; simplify in H'; apply H'; reflexivity;
+       | intros; lapply (IH ? H1) as H';
          (* XXX destruct H1 *)
          change in H' with (Not ((match (x1::tl1) with [nil⇒tl1|(cons _ l) ⇒ l]) = l)); 
-         rewrite > H1 in H'; simplify in H'; apply H'; reflexivity;
-       ]]]]
+         rewrite > H in H'; simplify in H'; apply H'; reflexivity;]]]]
 qed.
     
 definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).  
-  
+  
\ No newline at end of file
diff --git a/matita/library/technicalities/setoids.ma b/matita/library/technicalities/setoids.ma
index 0f3bda302..362b9fb5b 100644
--- a/matita/library/technicalities/setoids.ma
+++ b/matita/library/technicalities/setoids.ma
@@ -155,9 +155,7 @@ definition morphism_theory_of_function :
   generalize in match f; clear f;
   elim In;
    [ unfold make_compatibility_goal;
-     simplify;
-     intros;
-     whd;
+     whd; intros;
      reflexivity
    | simplify;
      intro;
@@ -612,26 +610,21 @@ theorem apply_morphism_compatibility_Right2Left:
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim t 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
-        simplify in H;
-        simplify in H1;
-        simplify;
         apply H;
         exact H1
       | intros 8 (v T1 r Hr m1 m2 args1 args2);
-        cases v;
+        cases v; 
+        simplify;
         intros (H H1);
-        simplify in H1;
-        apply H;
-        exact H1
+        apply (H ? ? H1);
       | intros;
         apply H1;
         exact H2
       | intros 7 (v);
-        cases v;
+        cases v; simplify;
         intros (H H1);
-        simplify in H1;
         apply H;
         exact H1
       | intros;
@@ -726,10 +719,9 @@ theorem apply_morphism_compatibility_Left2Right:
         directed_relation_of_relation_class Left2Right ?
          (apply_morphism ? ? m1 args1)
          (apply_morphism ? ? m2 args2).
-  intro;
-  elim In;
-   [ simplify in m1 m2 args1 args2 ⊢ %;
-     change in H1 with
+  intro; 
+  elim In 0; simplify; intros;
+   [ change in H1 with
       (directed_relation_of_argument_class
         (get_rewrite_direction Left2Right t) t args1 args2);
      generalize in match H1; clear H1;
@@ -738,11 +730,8 @@ theorem apply_morphism_compatibility_Left2Right:
      generalize in match args1; clear args1;
      generalize in match m2; clear m2;
      generalize in match m1; clear m1;
-     elim t 0;
+     elim t 0; simplify;
       [ intros (T1 r Hs Hr m1 m2 args1 args2 H H1);
-        simplify in H;
-        simplify in H1;
-        simplify;
         apply H;
         exact H1
       | intros 8 (v T1 r Hr m1 m2 args1 args2);
@@ -793,7 +782,6 @@ theorem apply_morphism_compatibility_Left2Right:
      generalize in match m1; clear m1;
      elim t 0;
       [ intros (T1 r Hs Hr m1 m2 H1 t1 t3 H3);
-        simplify in H3;
         change in H1 with
          (∀x1,x2:T1.r x1 x2 → make_compatibility_goal_aux n Out (m1 x1) (m2 x2));
      | intro v;