-(minus h2 k) n2) (aplus_gz_ge n2 k h2 (le_S_n k h2 (le_S (S k) h2 H2)))) in
-(let H5 \def (sym_eq A (ASort O (plus (minus k h1) n1)) (ASort (minus h2 k)
-n2) H4) in (let H6 \def (eq_ind nat (minus h2 k) (\lambda (n: nat).(eq A
-(ASort n n2) (ASort O (plus (minus k h1) n1)))) H5 (S (minus h2 (S k)))
-(minus_x_Sy h2 k H2)) in (let H7 \def (eq_ind A (ASort (S (minus h2 (S k)))
-n2) (\lambda (ee: A).(match ee in A return (\lambda (_: A).Prop) with [(ASort
-n _) \Rightarrow (match n in nat return (\lambda (_: nat).Prop) with [O
-\Rightarrow False | (S _) \Rightarrow True]) | (AHead _ _) \Rightarrow
-False])) I (ASort O (plus (minus k h1) n1)) H6) in (False_ind (leqz (ASort h1
-n1) (ASort h2 n2)) H7))))))) (\lambda (H2: (le h2 k)).(let H3 \def (eq_ind A
-(aplus gz (ASort h1 n1) k) (\lambda (a: A).(eq A a (aplus gz (ASort h2 n2)
-k))) H0 (ASort O (plus (minus k h1) n1)) (aplus_gz_le k h1 n1 H1)) in (let H4
-\def (eq_ind A (aplus gz (ASort h2 n2) k) (\lambda (a: A).(eq A (ASort O
-(plus (minus k h1) n1)) a)) H3 (ASort O (plus (minus k h2) n2)) (aplus_gz_le
-k h2 n2 H2)) in (let H5 \def (f_equal A nat (\lambda (e: A).(match e in A
-return (\lambda (_: A).nat) with [(ASort _ n) \Rightarrow n | (AHead _ _)
-\Rightarrow ((let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m:
-nat).(match n with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in
-plus) (minus k h1) n1)])) (ASort O (plus (minus k h1) n1)) (ASort O (plus
-(minus k h2) n2)) H4) in (let H_y \def (plus_plus k h1 h2 n1 n2 H1 H2 H5) in
-(leqz_sort h1 h2 n1 n2 H_y))))))))))))))) (\lambda (a0: A).(\lambda (a3:
-A).(\lambda (_: (leq gz a0 a3)).(\lambda (H1: (leqz a0 a3)).(\lambda (a4:
-A).(\lambda (a5: A).(\lambda (_: (leq gz a4 a5)).(\lambda (H3: (leqz a4
-a5)).(leqz_head a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).
-(* COMMENTS
-Initial nodes: 1375
-END *)
+(minus h2 k) n2) (aplus_gz_ge n2 k h2 (le_S_n k h2 (le_S_n (S k) (S h2) (le_S
+(S (S k)) (S h2) (le_n_S (S k) h2 H2)))))) in (let H5 \def (sym_eq A (ASort O
+(plus (minus k h1) n1)) (ASort (minus h2 k) n2) H4) in (let H6 \def (eq_ind
+nat (minus h2 k) (\lambda (n: nat).(eq A (ASort n n2) (ASort O (plus (minus k
+h1) n1)))) H5 (S (minus h2 (S k))) (minus_x_Sy h2 k H2)) in (let H7 \def
+(eq_ind A (ASort (S (minus h2 (S k))) n2) (\lambda (ee: A).(match ee with
+[(ASort n _) \Rightarrow (match n with [O \Rightarrow False | (S _)
+\Rightarrow True]) | (AHead _ _) \Rightarrow False])) I (ASort O (plus (minus
+k h1) n1)) H6) in (False_ind (leqz (ASort h1 n1) (ASort h2 n2)) H7)))))))
+(\lambda (H2: (le h2 k)).(let H3 \def (eq_ind A (aplus gz (ASort h1 n1) k)
+(\lambda (a: A).(eq A a (aplus gz (ASort h2 n2) k))) H0 (ASort O (plus (minus
+k h1) n1)) (aplus_gz_le k h1 n1 H1)) in (let H4 \def (eq_ind A (aplus gz
+(ASort h2 n2) k) (\lambda (a: A).(eq A (ASort O (plus (minus k h1) n1)) a))
+H3 (ASort O (plus (minus k h2) n2)) (aplus_gz_le k h2 n2 H2)) in (let H5 \def
+(f_equal A nat (\lambda (e: A).(match e with [(ASort _ n) \Rightarrow n |
+(AHead _ _) \Rightarrow (plus (minus k h1) n1)])) (ASort O (plus (minus k h1)
+n1)) (ASort O (plus (minus k h2) n2)) H4) in (let H_y \def (plus_plus k h1 h2
+n1 n2 H1 H2 H5) in (leqz_sort h1 h2 n1 n2 H_y))))))))))))))) (\lambda (a0:
+A).(\lambda (a3: A).(\lambda (_: (leq gz a0 a3)).(\lambda (H1: (leqz a0
+a3)).(\lambda (a4: A).(\lambda (a5: A).(\lambda (_: (leq gz a4 a5)).(\lambda
+(H3: (leqz a4 a5)).(leqz_head a0 a3 H1 a4 a5 H3))))))))) a1 a2 H))).