From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 19:04:18 +0000 (+0000)
Subject: Dummy dependent types are no longer cleaned in inductive type arities.
X-Git-Tag: make_still_working~5160
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f11316bd6cda8e0eb519bbced0a09de23dacc252;p=helm.git

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

diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index f5847033a..8e70ab958 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -727,10 +727,10 @@ elim k
                     |(*già usata 2 volte: fattorizzare*)
                      elim n
                        [simplify;apply le_n
-                       |apply (bool_elim ? (p n1));intro
+                       |apply (bool_elim ? (p n2));intro
                           [rewrite > true_to_pi_p_Sn
                              [rewrite > (times_n_O O);apply lt_times
-                                [elim (H n1);assumption
+                                [elim (H n2);assumption
                                 |assumption]
                              |assumption]
                           |rewrite > false_to_pi_p_Sn;assumption]]]
@@ -777,7 +777,7 @@ intros;apply eq_sigma_p;intros;
         [rewrite > exp_plus_times;
          unfold bc;
          elim (bc2 n x)
-           [rewrite > H3;cut (x!*n2 = pi_p x (\lambda i.true) (\lambda i.(n - i)))
+           [rewrite > H3;cut (x!*n1 = pi_p x (\lambda i.true) (\lambda i.(n - i)))
               [rewrite > sym_times in ⊢ (? ? (? (? (? (? % ?) ?) ?) ?) ?);
                rewrite > assoc_times;
                rewrite < sym_times in ⊢ (? ? (? (? (? % ?) ?) ?) ?);
@@ -878,25 +878,25 @@ intros;apply eq_sigma_p;intros;
                              [apply divides_SO_n
                              |elim x
                                 [simplify;apply divides_SO_n
-                                |change in \vdash (? % ?) with (n*(exp n n1));
+                                |change in \vdash (? % ?) with (n*(exp n n2));
                                  rewrite > true_to_pi_p_Sn
                                    [apply divides_times;assumption
                                    |reflexivity]]]
                           |apply lt_O_fact
-                          |apply (witness ? ? n2);symmetry;assumption]]
+                          |apply (witness ? ? n1);symmetry;assumption]]
                     |rewrite > divides_times_to_eq;
                        [apply eq_f2
                           [reflexivity
                           |elim x
                              [simplify;reflexivity
-                             |change in \vdash (? ? % ?) with (a*(exp a n1));
+                             |change in \vdash (? ? % ?) with (a*(exp a n2));
                               rewrite > true_to_pi_p_Sn
                                 [apply eq_f2
                                    [reflexivity
                                    |assumption]
                                 |reflexivity]]]
                        |apply lt_O_fact
-                       |apply (witness ? ? n2);symmetry;assumption]]
+                       |apply (witness ? ? n1);symmetry;assumption]]
                  |apply lt_O_fact
                  |apply lt_O_fact]
               |apply (inj_times_r (pred ((n-x)!)));
@@ -964,15 +964,15 @@ intros;transitivity ((exp a n)*(exp (S n) n)/(exp n n)/(exp a n))
            [elim H2;rewrite > H3;rewrite < times_exp;rewrite > sym_times in ⊢ (? ? (? (? ? ? (λ_:?.? ? %)) ?) ?);
             rewrite > sym_times in ⊢ (? ? ? (? ? ? (λ_:?.? (? (? ? %) ?) ?)));
             transitivity (sigma_p (S n) (λx:nat.true)
-(λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n2)\sup(n)))/exp n n)
+(λk:nat.(exp n n)*(bc n k*(n)\sup(n-k)*(n1)\sup(n)))/exp n n)
               [apply eq_f2
                  [apply eq_sigma_p;intros;
                     [reflexivity
                     |rewrite < assoc_times;rewrite > sym_times;reflexivity]
                  |reflexivity]
-              |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n2 n)));
+              |rewrite < (distributive_times_plus_sigma_p ? ? ? (\lambda k.bc n k*(exp n (n-k))*(exp n1 n)));
                transitivity (sigma_p (S n) (λx:nat.true)
-                (λk:nat.bc n k*(n2)\sup(n)*(n)\sup(n-k)))
+                (λk:nat.bc n k*(n1)\sup(n)*(n)\sup(n-k)))
                  [rewrite > (S_pred (exp n n))
                     [rewrite > div_times;apply eq_sigma_p;intros
                        [reflexivity
@@ -1042,7 +1042,7 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n)
                            rewrite > sym_times;apply divides_times
                              [apply divides_SO_n
                              |elim (bc2 n i);
-                                [apply (witness ? ? n2);
+                                [apply (witness ? ? n1);
                                  cut (pi_p i (\lambda y.true) (\lambda i.n-i) = (n!/(n-i)!))
                                    [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
                                     rewrite > (S_pred ((n-i)!))
@@ -1086,7 +1086,7 @@ intros;rewrite > (neper_sigma_p3 (n*S n) n)
                            apply divides_times
                              [apply divides_SO_n
                              |elim (bc2 (S n) i);
-                                [apply (witness ? ? n2);
+                                [apply (witness ? ? n1);
                                  cut (pi_p i (\lambda y.true) (\lambda i.S n-i) = ((S n)!/(S n-i)!))
                                    [rewrite > Hcut1;rewrite > H3;rewrite > sym_times in ⊢ (? ? (? (? % ?) ?) ?);
                                     rewrite > (S_pred ((S n-i)!))