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

diff --git a/helm/software/matita/library/Z/dirichlet_product.ma b/helm/software/matita/library/Z/dirichlet_product.ma
index 6328bc7dca8ca34f3a836d2f7b54af8a4a204ada..c45b4dc53443d1d3eb76e84044217bb1e5dc1dd1 100644 (file)
--- a/helm/software/matita/library/Z/dirichlet_product.ma
+++ b/helm/software/matita/library/Z/dirichlet_product.ma
@@ -257,7 +257,7 @@ apply (trans_eq ? ?
                        assumption
                       ]
                     |elim (divides_b_true_to_divides ? ? H4).
-                     apply (witness ? ? n2).
+                     apply (witness ? ? n1).
                      rewrite > assoc_times.
                      rewrite < H5.
                      rewrite < sym_times.

diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma
index 1765b38072626e02bd6593da9f31654ac0c36d22..1bb493f79c53010261116c3e7234df843700ab92 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev_teta.ma
+++ b/helm/software/matita/library/nat/chebyshev_teta.ma
@@ -162,7 +162,7 @@ elim (bc2 (S(2*m)) m)
   [unfold bc.rewrite > H3.
    rewrite > sym_times.
    rewrite > lt_O_to_div_times
-    [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n2)
+    [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n1)
       [apply False_ind.
        elim (divides_times_to_divides p (m!) (S (2*m)-m)!)
         [apply (lt_to_not_le ? ? (lt_to_le ? ? H1)).

diff --git a/helm/software/matita/library/nat/congruence.ma b/helm/software/matita/library/nat/congruence.ma
index 753745d4540d23f1378fcd3f4ac9cbc2791f14e0..948d10667261ddc7971811c359f65424a0741aef 100644 (file)
--- a/helm/software/matita/library/nat/congruence.ma
+++ b/helm/software/matita/library/nat/congruence.ma
@@ -118,7 +118,7 @@ qed.
 theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to 
 divides p (n - m) \to congruent n m p.
 intros.elim H2.
-apply (eq_times_plus_to_congruent n m p n2).
+apply (eq_times_plus_to_congruent n m p n1).
 assumption.
 rewrite < sym_plus.
 apply minus_to_plus.assumption.

diff --git a/helm/software/matita/library/nat/gcd_properties1.ma b/helm/software/matita/library/nat/gcd_properties1.ma
index bb8b9bb534881a1c019558c9212310bc669f2c72..776b38adfc5184c110482dc8fbdb700673579c1f 100644 (file)
--- a/helm/software/matita/library/nat/gcd_properties1.ma
+++ b/helm/software/matita/library/nat/gcd_properties1.ma
@@ -25,7 +25,7 @@ c \divides a \to c \divides b \to
 intros.
 elim (H2 ((gcd a b)))
 [ apply (antisymmetric_divides (gcd a b) c)
-  [ apply (witness (gcd a b) c n2).
+  [ apply (witness (gcd a b) c n1).
     assumption
   | apply divides_d_gcd;
       assumption
@@ -164,7 +164,7 @@ apply (nat_case1 a)
           ]
         | assumption
         ]
-      | apply (witness ? ? n2).
+      | apply (witness ? ? n1).
         apply (inj_times_r1 (gcd a b) Hcut1).
         rewrite < assoc_times.
         rewrite < sym_times in \vdash (? ? (? % ?) ?).
@@ -328,13 +328,13 @@ apply gcd1
 | intros.
   elim H1.
   elim H2.
-  cut(b = (d*n2) + a) 
-  [ cut (b - (d*n2) = a)
+  cut(b = (d*n1) + a) 
+  [ cut (b - (d*n1) = a)
     [ rewrite > H4 in Hcut1.
-      rewrite < (distr_times_minus d n n2) in Hcut1.
+      rewrite < (distr_times_minus d n n1) in Hcut1.
       apply divides_d_gcd
       [ assumption
-      | apply (witness d a (n - n2)).
+      | apply (witness d a (n - n1)).
         apply sym_eq.
         assumption
       ]

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 8da13d9ab08e7fdbb4d7f165e75394eb69af15b4..f5847033ab0305660fff7faa26f2a2852811e41f 100644 (file)
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -280,7 +280,7 @@ rewrite > lt_O_to_div_times
      assumption
     |apply lt_exp_Sn_n_SSSO
     ]
-  |apply (O_lt_times_to_O_lt ? n2).
+  |apply (O_lt_times_to_O_lt ? n1).
    rewrite < H2.
    assumption
   ]