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

[helm.git] / helm / software / matita / contribs / RELATIONAL / ZEq / setoid.ma

diff --git a/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
index 587470bfc70f9af0374199523a390485589f7f4d..a9c9d0763624957f7916b7d4e1ec8ad7e7ccd548 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
+++ b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
@@ -19,7 +19,7 @@ include "ZEq/defs.ma".
 
 theorem zeq_refl: \forall z. z = z.
  intros. elim z. clear z.
- lapply (nplus_total t t1). decompose.
+ lapply (nplus_total a b). decompose.
  autobatch.
 qed.