-H0 in le return (\lambda (n0: nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to
-P))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
-(eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_:
-nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in
-(False_ind P H2))) | (le_S m0 H1) \Rightarrow (\lambda (H2: (eq nat (S m0)
-O)).((let H3 \def (eq_ind nat (S m0) (\lambda (e: nat).(match e in nat return
-(\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True]))
-I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) in (H1 (refl_equal
-nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P:
-Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind
-(\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n))
-\to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S
-O) (S n))).(let H2 \def (match H0 in le return (\lambda (n1: nat).(\lambda
-(_: (le ? n1)).((eq nat n1 O) \to P))) with [le_n \Rightarrow (\lambda (H2:
-(eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e
-in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _)
-\Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow
-(\lambda (H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda
-(e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
-False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m0) \to P)
-H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_:
-((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda
-(P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S
-n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
-(* COMMENTS
-Initial nodes: 409
-END *)
-
-theorem le_Sx_x:
+H0 with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def
+(eq_ind nat (S n) (\lambda (e: nat).(match e with [O \Rightarrow False | (S
+_) \Rightarrow True])) I O H1) in (False_ind P H2))) | (le_S m0 H1)
+\Rightarrow (\lambda (H2: (eq nat (S m0) O)).((let H3 \def (eq_ind nat (S m0)
+(\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) in (H1
+(refl_equal nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0:
+nat).(\forall (P: Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda
+(n0: nat).(nat_ind (\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to
+((le (S n1) (S n)) \to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n)
+O)).(\lambda (_: (le (S O) (S n))).(let H2 \def (match H0 with [le_n
+\Rightarrow (\lambda (H2: (eq nat (S n) O)).(let H3 \def (eq_ind nat (S n)
+(\lambda (e: nat).(match e with [O \Rightarrow False | (S _) \Rightarrow
+True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow (\lambda
+(H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda (e:
+nat).(match e with [O \Rightarrow False | (S _) \Rightarrow True])) I O H3)
+in (False_ind ((le (S n) m0) \to P) H4)) H2))]) in (H2 (refl_equal nat
+O)))))) (\lambda (n1: nat).(\lambda (_: ((\forall (P: Prop).((le (S n) n1)
+\to ((le (S n1) (S n)) \to P))))).(\lambda (P: Prop).(\lambda (H1: (le (S n)
+(S n1))).(\lambda (H2: (le (S (S n1)) (S n))).(H n1 P (le_S_n n n1 H1)
+(le_S_n (S n1) n H2))))))) n0)))) m).
+
+lemma le_Sx_x: