-\def (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat
-n O) \to (eq bool (blt y O) true)))) with [le_n \Rightarrow (\lambda (H0: (eq
-nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e in
-nat return (\lambda (_: nat).Prop) 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 in nat return (\lambda (_: nat).Prop)
-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).
-(* COMMENTS
-Initial nodes: 291
-END *)
+\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).