X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdecidable_kit%2Ffintype.ma;h=82d54131bb494901801a8d3162382a76281b7fd6;hb=347b0f483245bd0295f95f99742e23484c331312;hp=9c5e1a843c6f1934ca91801b5ade553efbcf3ed5;hpb=59d7f64e2e1a22ded8f9017942ca640fe62d886a;p=helm.git

diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
index 9c5e1a843..82d54131b 100644
--- a/helm/software/matita/library/decidable_kit/fintype.ma
+++ b/helm/software/matita/library/decidable_kit/fintype.ma
@@ -84,11 +84,13 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
  [ apply (mk_finType fsort enum Hcut)
  | intros (x); cases x (n Hn); simplify in Hn; clear x;
    generalize in match Hn; generalize in match Hn; clear Hn;
+   unfold enum;
    unfold segment_enum;
    generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
    intros 1 (m); elim m  (Hm Hn p IH Hm Hn); [ simplify in Hm; destruct Hm ]
    simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
-   [1:unfold segment in ⊢ (? ? match ? % ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
+   [1:unfold fsort;
+      unfold segment in ⊢ (? ? match ? % ? ? with [_ ⇒ ?|_ ⇒ ?] ?);
       unfold nat_eqType in ⊢ (? ? match % with [_ ⇒ ?|_ ⇒ ?] ?);
       simplify; apply (cmpP nat_eqType n p); intros (Enp); simplify;
       [2:rewrite > IH; [1,3: autobatch]
@@ -104,8 +106,8 @@ cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
          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;
+         generalize in match H1; clear H1; cases s (r Pr); clear s; intros (H1);
+         unfold fsort; 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]
@@ -135,7 +137,7 @@ 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; simplify; [reflexivity]
-apply (cmpP d x t); intros (E); simplify ; rewrite > E; [reflexivity]
+apply (cmpP d x t); intros (E); simplify ; try rewrite > E; [reflexivity]
 rewrite > andbA; rewrite > andbC in ⊢ (? ? (? % ?) ?); rewrite < andbA;
 rewrite < H; rewrite > andbC in ⊢ (? ? ? (? % ?)); rewrite < andbA; reflexivity;
 qed.
@@ -153,9 +155,9 @@ intros (d l); apply prove_reflect; elim l; [1: simplify in H1; destruct H1 | 3:
     [2: lapply (uniq_mem ? ? ? H1) as H4; simplify; apply (cmpP d x t);  
         intros (H5); simplify;
         [1: rewrite > count_O; [reflexivity]
-            intros (y Hy); rewrite > H5 in H2 H3 H4 ⊢ %; clear H5; clear x; 
+            intros (y Hy); rewrite > H5 in H2 H3 ⊢ %; clear H5; clear x; 
             rewrite > H2 in H4; destruct H4;
-         |2: simplify; rewrite > H5; simplify; apply H; 
+         |2: simplify; apply H; 
              rewrite > uniq_tail in H1; cases (b2pT ? ? (andbP ? ?) H1); 
              assumption;]
     |1: simplify; rewrite > H2; simplify; rewrite > count_O; [reflexivity]