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)