indentation

diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma
index 0156a98cadea4856ff10761233958ad107516c24..b600072c61ba97cfa9e862251d04c566b3a0e765 100644 (file)
--- a/helm/matita/library/nat/nat.ma
+++ b/helm/matita/library/nat/nat.ma
@@ -83,9 +83,10 @@ qed.
 
 theorem nat_elim2 :
  \forall R:nat \to nat \to Prop.
-  (\forall n:nat. R O n) \to 
-  (\forall n:nat. R (S n) O) \to 
-  (\forall n,m:nat. R n m \to R (S n) (S m)) \to \forall n,m:nat. R n m.
+  (\forall n:nat. R O n) 
+  \to (\forall n:nat. R (S n) O) 
+  \to (\forall n,m:nat. R n m \to R (S n) (S m))
+  \to \forall n,m:nat. R n m.
 intros 5;elim n 
   [ apply H
   | apply (nat_case m)