- \lambda (k: K).(\lambda (i: nat).(let TMP_1 \def (r k i) in (let TMP_2 \def
-(S TMP_1) in (let TMP_6 \def (\lambda (n: nat).(let TMP_3 \def (S O) in (let
-TMP_4 \def (minus n TMP_3) in (let TMP_5 \def (r k i) in (eq nat TMP_4
-TMP_5))))) in (let TMP_7 \def (r k i) in (let TMP_9 \def (\lambda (n:
-nat).(let TMP_8 \def (r k i) in (eq nat n TMP_8))) in (let TMP_10 \def (r k
-i) in (let TMP_11 \def (refl_equal nat TMP_10) in (let TMP_12 \def (r k i) in
-(let TMP_13 \def (S TMP_12) in (let TMP_14 \def (S O) in (let TMP_15 \def
-(minus TMP_13 TMP_14) in (let TMP_16 \def (r k i) in (let TMP_17 \def
-(minus_Sx_SO TMP_16) in (let TMP_18 \def (eq_ind_r nat TMP_7 TMP_9 TMP_11
-TMP_15 TMP_17) in (let TMP_19 \def (S i) in (let TMP_20 \def (r k TMP_19) in
-(let TMP_21 \def (r_S k i) in (eq_ind_r nat TMP_2 TMP_6 TMP_18 TMP_20
-TMP_21))))))))))))))))))).
-
-theorem r_arith1:
+ \lambda (k: K).(\lambda (i: nat).(eq_ind_r nat (S (r k i)) (\lambda (n:
+nat).(eq nat (minus n (S O)) (r k i))) (eq_ind_r nat (r k i) (\lambda (n:
+nat).(eq nat n (r k i))) (refl_equal nat (r k i)) (minus (S (r k i)) (S O))
+(minus_Sx_SO (r k i))) (r k (S i)) (r_S k i))).
+
+lemma r_arith1: