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

diff --git a/helm/software/matita/library/algebra/CoRN/Setoids.ma b/helm/software/matita/library/algebra/CoRN/Setoids.ma
index ddbb807a85643681b923fc6ee91afb367b0d6c50..3b37dc42b069e329270626d8f624e9b3f8d59249 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/Setoids.ma
+++ b/helm/software/matita/library/algebra/CoRN/Setoids.ma
@@ -237,8 +237,8 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
    unfold prod_ap. simplify.
    intros.
    elim H
-   [apply (ap_irreflexive A t H1)
-   |apply (ap_irreflexive B t1 H1)
+   [apply (ap_irreflexive A a H1)
+   |apply (ap_irreflexive B b H1)
    ]
  |unfold.
   intros 2.
@@ -258,14 +258,14 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
   unfold prod_ap in H. simplify in H.
   unfold prod_ap. simplify.
   elim H
-  [cut ((t \neq t4) \or (t4 \neq t2))
+  [cut ((a \neq a2) \or (a2 \neq a1))
    [elim Hcut
     [left. left. assumption
     |right. left. assumption
     ]
    |apply (ap_cotransitive A). assumption
    ]
-  |cut ((t1 \neq t5) \or (t5 \neq t3))
+  |cut ((b \neq b2) \or (b2 \neq b1))
    [elim Hcut
     [left. right. assumption
     |right. right. assumption
@@ -291,8 +291,8 @@ apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
  |intro. unfold. intro.
  elim H.
  elim H1
-  [apply (eq_imp_not_ap A t t2 H2). assumption
-  |apply (eq_imp_not_ap B t1 t3 H3). assumption
+  [apply (eq_imp_not_ap A a a1 H2). assumption
+  |apply (eq_imp_not_ap B b b1 H3). assumption
   ]
  ]
 ]