From a877debee863033e33a0f7d497e253ad3b076477 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 26 Jan 2006 17:51:06 +0000 Subject: [PATCH] indentation --- helm/matita/library/nat/nat.ma | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/matita/library/nat/nat.ma b/helm/matita/library/nat/nat.ma index 0156a98ca..b600072c6 100644 --- 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) -- 2.39.2