X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fgeneric_sigma_p.ma;h=8ab37e999fd6f39ccd9dbf8918599bd204d1ff55;hb=dfbd010fe5a46d049849913bc23000289893ea4f;hp=ed9f59b0a52fbcc6182712050c26291862e30b14;hpb=c3bba4af040f8040e5eae07e70690c52f8c614f8;p=helm.git

diff --git a/matita/library/nat/generic_sigma_p.ma b/matita/library/nat/generic_sigma_p.ma
index ed9f59b0a..8ab37e999 100644
--- a/matita/library/nat/generic_sigma_p.ma
+++ b/matita/library/nat/generic_sigma_p.ma
@@ -982,7 +982,7 @@ theorem distributive_times_plus_sigma_p_generic: \forall A:Type.
   \to
 
 ((timesA k (sigma_p_gen n p A g basePlusA plusA)) = 
- (sigma_p_gen n p A (\lambda i:nat.(timesA (g i) k)) basePlusA plusA)).
+ (sigma_p_gen n p A (\lambda i:nat.(timesA k (g i))) basePlusA plusA)).
 intros.
 elim n
 [ simplify.