simplify.
intros.
rewrite > pred_Sn.
-rewrite > pred_Sn y.
+rewrite > (pred_Sn y).
apply eq_f. assumption.
qed.
(\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.apply H1.
+apply (nat_case m).apply H1.
intros.apply H2. apply H3.
qed.
theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
intros.simplify.
-apply nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))).
+apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False)))).
intro.elim n1.
left.reflexivity.
right.apply not_eq_O_S.
intro.right.intro.
-apply not_eq_O_S n1.
+apply (not_eq_O_S n1).
apply sym_eq.assumption.
intros.elim H.
left.apply eq_f. assumption.