little bug in coercion generation found. it use to create more coercions that expecte...

[helm.git] / matita / library / nat / generic_sigma_p.ma

diff --git a/matita/library/nat/generic_sigma_p.ma b/matita/library/nat/generic_sigma_p.ma
index ed9f59b0a52fbcc6182712050c26291862e30b14..8ab37e999fd6f39ccd9dbf8918599bd204d1ff55 100644 (file)
--- 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.