X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FZ%2Fsigma_p.ma;h=b246b8444f0cafed9f6c69a4640b955f8de38b0b;hb=8665d6bd01e0723b0867655ac8c909eb4017f964;hp=92b21539605e564044f85b67228b61d0077b627f;hpb=d5afc8f8891d0020f5804eb2322fc0d1c8c60702;p=helm.git

diff --git a/helm/software/matita/library/Z/sigma_p.ma b/helm/software/matita/library/Z/sigma_p.ma
index 92b215396..b246b8444 100644
--- a/helm/software/matita/library/Z/sigma_p.ma
+++ b/helm/software/matita/library/Z/sigma_p.ma
@@ -168,7 +168,7 @@ theorem eq_sigma_p_gh:
 (\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
 (\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
 (\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
-sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 (\lambda x.p2 x) g.
+sigma_p n p1 (\lambda x.g(h x)) = sigma_p n1 p2 g.
 intros.
 unfold sigma_p.
 apply (eq_iter_p_gen_gh Z OZ Zplus ? ? ? g h h1 n n1 p1 p2)