- \lambda (x: nat).(let TMP_793 \def (\lambda (n: nat).(\forall (y: nat).((lt
-y n) \to (let TMP_792 \def (blt y n) in (eq bool TMP_792 true))))) in (let
-TMP_791 \def (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 \def (match H
-in le with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let TMP_787
-\def (S y) in (let TMP_786 \def (\lambda (e: nat).(match e in nat with [O
-\Rightarrow False | (S _) \Rightarrow True])) in (let H1 \def (eq_ind nat
-TMP_787 TMP_786 I O H0) in (let TMP_788 \def (blt y O) in (let TMP_789 \def
-(eq bool TMP_788 true) in (False_ind TMP_789 H1))))))) | (le_S m H0)
-\Rightarrow (\lambda (H1: (eq nat (S m) O)).(let TMP_782 \def (S m) in (let
-TMP_781 \def (\lambda (e: nat).(match e in nat with [O \Rightarrow False | (S
-_) \Rightarrow True])) in (let H2 \def (eq_ind nat TMP_782 TMP_781 I O H1) in
-(let TMP_784 \def ((le (S y) m) \to (let TMP_783 \def (blt y O) in (eq bool
-TMP_783 true))) in (let TMP_785 \def (False_ind TMP_784 H2) in (TMP_785
-H0)))))))]) in (let TMP_790 \def (refl_equal nat O) in (H0 TMP_790))))) in
-(let TMP_780 \def (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n)
-\to (eq bool (blt y n) true))))).(\lambda (y: nat).(let TMP_779 \def (\lambda
-(n0: nat).((lt n0 (S n)) \to (let TMP_777 \def (S n) in (let TMP_778 \def
-(blt n0 TMP_777) in (eq bool TMP_778 true))))) in (let TMP_776 \def (\lambda
-(_: (lt O (S n))).(refl_equal bool true)) in (let TMP_775 \def (\lambda (n0:
-nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool (match n0 with [O \Rightarrow
-true | (S m) \Rightarrow (blt m n)]) true)))).(\lambda (H1: (lt (S n0) (S
-n))).(let TMP_773 \def (S n0) in (let TMP_774 \def (le_S_n TMP_773 n H1) in
-(H n0 TMP_774)))))) in (nat_ind TMP_779 TMP_776 TMP_775 y))))))) in (nat_ind
-TMP_793 TMP_791 TMP_780 x)))).
+ \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to
+(eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0
+\def (match H with [le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1
+\def (eq_ind nat (S y) (\lambda (e: nat).(match e with [O \Rightarrow False |
+(S _) \Rightarrow True])) I O H0) in (False_ind (eq bool (blt y O) true)
+H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def
+(eq_ind nat (S m) (\lambda (e: nat).(match e with [O \Rightarrow False | (S
+_) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq bool (blt
+y O) true)) H2)) H0))]) in (H0 (refl_equal nat O))))) (\lambda (n:
+nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq bool (blt y n)
+true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: nat).((lt n0 (S n)) \to
+(eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S n))).(refl_equal bool
+true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) \to (eq bool (match n0
+with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true)))).(\lambda
+(H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1))))) y)))) x).