Dummy dependent types are no longer cleaned in inductive type arities.

diff --git a/helm/software/matita/library/nat/bertrand.ma b/helm/software/matita/library/nat/bertrand.ma
index d1ad9e12e923e29edec3a166fac4f9e528c55404..4d8596b6ebea5b1b22413022a5c78f5ea2f5a3f9 100644 (file)
--- a/helm/software/matita/library/nat/bertrand.ma
+++ b/helm/software/matita/library/nat/bertrand.ma
@@ -94,7 +94,7 @@ intro.elim t 0
         |intro;elim (H1 p);split;intros
            [elim (H6 H8);assumption
            |apply (H7 H8 H9);intros;elim (not_in_list_nil ? ? H10)]]
-     |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b t1 x))) (t1::l1))
+     |simplify;elim (H k (filter ? l (\lambda x.notb (divides_b a x))) (a::l1))
         [split;
            [assumption
            |intro;apply H8;]
@@ -103,13 +103,13 @@ intro.elim t 0
               [rewrite > H8;split
                  [split
                     [unfold;intros;split
-                       [elim (H3 t1);elim H9
+                       [elim (H3 a);elim H9
                           [elim H11;assumption
                           |apply in_list_head]
                        |intros;elim (le_to_or_lt_eq ? ? (divides_to_le ? ? ? H9))
                           [elim (divides_to_prime_divides ? ? H10 H11 H9);elim H12;
-                           elim H13;clear H13 H12;elim (H3 t1);elim H12
-                             [clear H13 H12;elim (H18 ? ? H14);elim (H2 a);
+                           elim H13;clear H13 H12;elim (H3 a);elim H12
+                             [clear H13 H12;elim (H18 ? ? H14);elim (H2 a1);
                               apply H13
                                 [assumption
                                 |elim H17;apply (trans_le ? ? ? ? H20);
@@ -122,48 +122,48 @@ intro.elim t 0
                                       [rewrite > H20;apply le_n
                                       |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);assumption]]]
                              |apply in_list_head]
-                          |elim (H3 t1);elim H11
+                          |elim (H3 a);elim H11
                              [elim H13;apply lt_to_le;assumption
                              |apply in_list_head]
                           |assumption]]
-                    |elim (H3 t1);elim H9
+                    |elim (H3 a);elim H9
                        [elim H11;assumption
                        |apply in_list_head]]
-                 |intros;elim (le_to_or_lt_eq t1 x)
+                 |intros;elim (le_to_or_lt_eq a x)
                     [assumption
                     |rewrite > H10 in H9;lapply (in_list_filter_to_p_true ? ? ? H9);
                      lapply (divides_n_n x);
                      rewrite > (divides_to_divides_b_true ? ? ? Hletin1) in Hletin
                        [simplify in Hletin;destruct Hletin
-                       |rewrite < H10;elim (H3 t1);elim H11
+                       |rewrite < H10;elim (H3 a);elim H11
                           [elim H13;apply lt_to_le;assumption
                           |apply in_list_head]]
                     |apply lt_to_le;apply (sorted_to_minimum ? ? ? ? H6);apply (in_list_filter ? ? ? H9)]]
                  |elim (H2 p);elim (H9 H8);split
                     [assumption
                     |intros;apply H12;apply in_list_cons;apply (in_list_filter ? ? ? H13)]]
-           |elim (decidable_eq_nat p t1)
+           |elim (decidable_eq_nat p a)
               [rewrite > H10;apply in_list_head
               |apply in_list_cons;elim (H2 p);apply (H12 H7 H8);intros;
-               apply (trans_le ? t1)
-                 [elim (decidable_lt p t1)
+               apply (trans_le ? a)
+                 [elim (decidable_lt p a)
                     [assumption
                     |lapply (not_lt_to_le ? ? H14);
-                     lapply (decidable_divides t1 p)
+                     lapply (decidable_divides a p)
                        [elim Hletin1
                           [elim H7;lapply (H17 ? H15)
                              [elim H10;symmetry;assumption
-                             |elim (H3 t1);elim H18
+                             |elim (H3 a);elim H18
                                 [elim H20;assumption
                                 |apply in_list_head]]
                           |elim (Not_lt_n_n p);apply H9;apply in_list_filter_r
-                             [elim (H3 p);apply (in_list_tail ? ? t1)
+                             [elim (H3 p);apply (in_list_tail ? ? a)
                                 [apply H17
                                    [apply prime_to_lt_SO;assumption
                                    |assumption
                                    |intros;elim H7;intro;lapply (H20 ? H21)
                                       [rewrite > Hletin2 in H18;elim (H11 H18);
-                                       lapply (H23 t1)
+                                       lapply (H23 a)
                                          [elim (lt_to_not_le ? ? Hletin3 Hletin)
                                          |apply in_list_head]
                                       |apply prime_to_lt_SO;elim (H2 p1);elim (H22 H18);
@@ -171,10 +171,10 @@ intro.elim t 0
                                 |unfold;intro;apply H15;rewrite > H18;apply divides_n_n]
                              |rewrite > (not_divides_to_divides_b_false ? ? ? H15);
                                 [reflexivity
-                                |elim (H3 t1);elim H16
+                                |elim (H3 a);elim H16
                                    [elim H18;apply lt_to_le;assumption
                                    |apply in_list_head]]]]
-                       |elim (H3 t1);elim H15
+                       |elim (H3 a);elim H15
                           [elim H17;apply lt_to_le;assumption
                           |apply in_list_head]]]
                  |elim (in_list_cons_case ? ? ? ? H13)
@@ -189,7 +189,7 @@ intro.elim t 0
                   [rewrite > H11;intro;lapply (in_list_filter_to_p_true ? ? ? H9);
                    rewrite > (divides_to_divides_b_true ? ? ? H12) in Hletin
                      [simplify in Hletin;destruct Hletin
-                     |elim (H3 t1);elim H13
+                     |elim (H3 a);elim H13
                         [elim H15;apply lt_to_le;assumption
                         |apply in_list_head]]
                   |elim H7
@@ -204,10 +204,10 @@ intro.elim t 0
                |intros;apply H11;apply in_list_cons;assumption
                |apply in_list_filter_r;
                   [assumption
-                  |lapply (H11 t1)
+                  |lapply (H11 a)
                      [rewrite > (not_divides_to_divides_b_false ? ? ? Hletin);
                         [reflexivity
-                        |elim (H3 t1);elim H13
+                        |elim (H3 a);elim H13
                            [elim H15;apply lt_to_le;assumption
                            |apply in_list_head]]
                      |apply in_list_head]]]]
@@ -219,7 +219,7 @@ intro.elim t 0
              apply H11;apply in_list_head]
          |generalize in match (sorted_cons_to_sorted ? ? ? ? H6);elim l
             [simplify;assumption
-            |simplify;elim (notb (divides_b t1 t2));simplify
+            |simplify;elim (notb (divides_b a a1));simplify
                [lapply (sorted_cons_to_sorted ? ? ? ? H8);lapply (H7 Hletin);
                 apply (sort_cons ? ? ? ? Hletin1);intros;
                 apply (sorted_to_minimum ? ? ? ? H8);apply (in_list_filter ? ? ? H9);
@@ -396,7 +396,7 @@ let rec checker l \def
 lemma checker_cons : \forall t,l.checker (t::l) = true \to checker l = true.
 intros 2;simplify;intro;generalize in match H;elim l
   [reflexivity
-  |change in H2 with (andb (checker (t1::l1)) (leb t (t1+(t1+O))) = true);
+  |change in H2 with (andb (checker (a::l1)) (leb t (a+(a+O))) = true);
    apply (andb_true_true ? ? H2)]
 qed.
 
@@ -561,7 +561,7 @@ intro.elim l 2
         |rewrite > H1.assumption
         ]
       |elim (H H6 p H1 H3).clear H.
-       apply (ex_intro ? ? a). 
+       apply (ex_intro ? ? a1). 
        elim H8.clear H8.
        elim H.clear H.
        split