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

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 ddbb807a8..3b37dc42b 100644
--- 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
   ]
  ]
 ]