-n))))).(\lambda (H0: (le (S k0) (S n0))).(ex2_ind nat (\lambda (n1: nat).(eq
-nat (S n0) (S n1))) (\lambda (n1: nat).(le k0 n1)) (eq A (asucc gz (aplus gz
-(ASort (S n0) n) k0)) (ASort (minus n0 k0) n)) (\lambda (x: nat).(\lambda
-(H1: (eq nat (S n0) (S x))).(\lambda (H2: (le k0 x)).(let H3 \def (f_equal
-nat nat (\lambda (e: nat).(match e in nat return (\lambda (_: nat).nat) with
-[O \Rightarrow n0 | (S n1) \Rightarrow n1])) (S n0) (S x) H1) in (let H4 \def
-(eq_ind_r nat x (\lambda (n1: nat).(le k0 n1)) H2 n0 H3) in (eq_ind A (aplus
-gz (ASort n0 n) k0) (\lambda (a: A).(eq A (asucc gz (aplus gz (ASort (S n0)
-n) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n0) n)) k0) (\lambda (a:
-A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus gz (ASort n0 n)
-k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc gz k0 (ASort (S
-n0) n))) (ASort (minus n0 k0) n) (IH n0 H4))))))) (le_gen_S k0 (S n0) H0)))))
-h)))) k)).
+n))))).(\lambda (H0: (le (S k0) (S n0))).(let H_y \def (le_S_n k0 n0 H0) in
+(eq_ind A (aplus gz (ASort n0 n) k0) (\lambda (a: A).(eq A (asucc gz (aplus
+gz (ASort (S n0) n) k0)) a)) (eq_ind A (aplus gz (asucc gz (ASort (S n0) n))
+k0) (\lambda (a: A).(eq A a (aplus gz (ASort n0 n) k0))) (refl_equal A (aplus
+gz (ASort n0 n) k0)) (asucc gz (aplus gz (ASort (S n0) n) k0)) (aplus_asucc
+gz k0 (ASort (S n0) n))) (ASort (minus n0 k0) n) (IH n0 H_y)))))) h)))) k)).