definition lt:
nat \to (nat \to Prop)
\def
- \lambda (n: nat).(\lambda (m: nat).(let TMP_1 \def (S n) in (le TMP_1 m))).
+ \lambda (n: nat).(\lambda (m: nat).(le (S n) m)).
definition IsSucc:
nat \to Prop
\lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
let rec plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with
-[O \Rightarrow m | (S p) \Rightarrow (let TMP_1 \def (plus p m) in (S
-TMP_1))]).
+[O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
let rec minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with
[O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) | (S
\forall (A: Type[0]).(((A \to nat)) \to (A \to (A \to Prop)))
\def
\lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(\lambda (a: A).(\lambda
-(b: A).(let TMP_1 \def (f a) in (let TMP_2 \def (f b) in (lt TMP_1
-TMP_2)))))).
+(b: A).(lt (f a) (f b))))).