.ma inclusions corrected/minimized

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

diff --git a/helm/matita/library/nat/sigma_and_pi.ma b/helm/matita/library/nat/sigma_and_pi.ma
index b9b8065aa6732ea934d5fcdac6289557d9852a29..29df3a1dfdab2b76f726748897621bd7758dd3d1 100644 (file)
--- a/helm/matita/library/nat/sigma_and_pi.ma
+++ b/helm/matita/library/nat/sigma_and_pi.ma
@@ -24,7 +24,4 @@ let rec sigma n f \def
 let rec pi n f \def
   match n with 
   [ O \Rightarrow (S O)
-  | (S p) \Rightarrow (f p)*(pi p f)].
-
-
-
+  | (S p) \Rightarrow (f p)*(pi p f)].
\ No newline at end of file