-(minus O (S z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda
-(n: nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H2: (eq
-nat O (S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O (\lambda
-(ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow
-True | (S _) \Rightarrow False])) I (S x1) H2) in (False_ind (eq nat (S x0)
-O) H4))))) (le_gen_S z0 O H0))))) (\lambda (y0: nat).(\lambda (_: (((le (S
-z0) (S x0)) \to ((le (S z0) y0) \to ((eq nat (minus (S x0) (S z0)) (minus y0
-(S z0))) \to (eq nat (S x0) y0)))))).(\lambda (H: (le (S z0) (S
-x0))).(\lambda (H0: (le (S z0) (S y0))).(\lambda (H1: (eq nat (minus (S x0)
-(S z0)) (minus (S y0) (S z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0
-x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z).
+(minus O (S z0)))).(let H_y \def (le_S_n z0 x0 H) in (ex2_ind nat (\lambda
+(n: nat).(eq nat O (S n))) (\lambda (n: nat).(le z0 n)) (eq nat (S x0) O)
+(\lambda (x1: nat).(\lambda (H2: (eq nat O (S x1))).(\lambda (_: (le z0
+x1)).(let H4 \def (eq_ind nat O (\lambda (ee: nat).(match ee in nat return
+(\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) \Rightarrow False]))
+I (S x1) H2) in (False_ind (eq nat (S x0) O) H4))))) (le_gen_S z0 O H0))))))
+(\lambda (y0: nat).(\lambda (_: (((le (S z0) (S x0)) \to ((le (S z0) y0) \to
+((eq nat (minus (S x0) (S z0)) (minus y0 (S z0))) \to (eq nat (S x0)
+y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S
+y0))).(\lambda (H1: (eq nat (minus (S x0) (S z0)) (minus (S y0) (S
+z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0)
+H1))))))) y)))) x)))) z).