-A).(\lambda (H1: (aprem i (ASort h2 n2) b2)).(let H2 \def (match H1 in aprem
-return (\lambda (n: nat).(\lambda (a: A).(\lambda (a0: A).(\lambda (_: (aprem
-n a a0)).((eq nat n i) \to ((eq A a (ASort h2 n2)) \to ((eq A a0 b2) \to (ex2
-A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem i (ASort h1 n1)
-b1)))))))))) with [(aprem_zero a0 a3) \Rightarrow (\lambda (H2: (eq nat O
-i)).(\lambda (H3: (eq A (AHead a0 a3) (ASort h2 n2))).(\lambda (H4: (eq A a0
-b2)).(eq_ind nat O (\lambda (n: nat).((eq A (AHead a0 a3) (ASort h2 n2)) \to
-((eq A a0 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
-A).(aprem n (ASort h1 n1) b1)))))) (\lambda (H5: (eq A (AHead a0 a3) (ASort
-h2 n2))).(let H6 \def (eq_ind A (AHead a0 a3) (\lambda (e: A).(match e in A
-return (\lambda (_: A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _
-_) \Rightarrow True])) I (ASort h2 n2) H5) in (False_ind ((eq A a0 b2) \to
-(ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem O (ASort h1
-n1) b1)))) H6))) i H2 H3 H4)))) | (aprem_succ a0 a i0 H2 a3) \Rightarrow
-(\lambda (H3: (eq nat (S i0) i)).(\lambda (H4: (eq A (AHead a3 a0) (ASort h2
-n2))).(\lambda (H5: (eq A a b2)).(eq_ind nat (S i0) (\lambda (n: nat).((eq A
-(AHead a3 a0) (ASort h2 n2)) \to ((eq A a b2) \to ((aprem i0 a0 a) \to (ex2 A
-(\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem n (ASort h1 n1)
-b1))))))) (\lambda (H6: (eq A (AHead a3 a0) (ASort h2 n2))).(let H7 \def
-(eq_ind A (AHead a3 a0) (\lambda (e: A).(match e in A return (\lambda (_:
-A).Prop) with [(ASort _ _) \Rightarrow False | (AHead _ _) \Rightarrow
-True])) I (ASort h2 n2) H6) in (False_ind ((eq A a b2) \to ((aprem i0 a0 a)
-\to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem (S i0)
-(ASort h1 n1) b1))))) H7))) i H3 H4 H5 H2))))]) in (H2 (refl_equal nat i)
-(refl_equal A (ASort h2 n2)) (refl_equal A b2)))))))))))) (\lambda (a0:
-A).(\lambda (a3: A).(\lambda (H0: (leq g a0 a3)).(\lambda (_: ((\forall (i:
-nat).(\forall (b2: A).((aprem i a3 b2) \to (ex2 A (\lambda (b1: A).(leq g b1
-b2)) (\lambda (b1: A).(aprem i a0 b1)))))))).(\lambda (a4: A).(\lambda (a5:
-A).(\lambda (_: (leq g a4 a5)).(\lambda (H3: ((\forall (i: nat).(\forall (b2:
-A).((aprem i a5 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
-A).(aprem i a4 b1)))))))).(\lambda (i: nat).(\lambda (b2: A).(\lambda (H4:
-(aprem i (AHead a3 a5) b2)).(nat_ind (\lambda (n: nat).((aprem n (AHead a3
-a5) b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem n
-(AHead a0 a4) b1))))) (\lambda (H5: (aprem O (AHead a3 a5) b2)).(let H6 \def
-(match H5 in aprem return (\lambda (n: nat).(\lambda (a: A).(\lambda (a6:
-A).(\lambda (_: (aprem n a a6)).((eq nat n O) \to ((eq A a (AHead a3 a5)) \to
-((eq A a6 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
-A).(aprem O (AHead a0 a4) b1)))))))))) with [(aprem_zero a6 a7) \Rightarrow
-(\lambda (_: (eq nat O O)).(\lambda (H7: (eq A (AHead a6 a7) (AHead a3
-a5))).(\lambda (H8: (eq A a6 b2)).((let H9 \def (f_equal A A (\lambda (e:
-A).(match e in A return (\lambda (_: A).A) with [(ASort _ _) \Rightarrow a7 |
-(AHead _ a) \Rightarrow a])) (AHead a6 a7) (AHead a3 a5) H7) in ((let H10
-\def (f_equal A A (\lambda (e: A).(match e in A return (\lambda (_: A).A)
-with [(ASort _ _) \Rightarrow a6 | (AHead a _) \Rightarrow a])) (AHead a6 a7)
-(AHead a3 a5) H7) in (eq_ind A a3 (\lambda (a: A).((eq A a7 a5) \to ((eq A a
-b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem O
-(AHead a0 a4) b1)))))) (\lambda (H11: (eq A a7 a5)).(eq_ind A a5 (\lambda (_:
-A).((eq A a3 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
-A).(aprem O (AHead a0 a4) b1))))) (\lambda (H12: (eq A a3 b2)).(eq_ind A b2
-(\lambda (_: A).(ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1:
-A).(aprem O (AHead a0 a4) b1)))) (eq_ind A a3 (\lambda (a: A).(ex2 A (\lambda
-(b1: A).(leq g b1 a)) (\lambda (b1: A).(aprem O (AHead a0 a4) b1))))
+A).(\lambda (H1: (aprem i (ASort h2 n2) b2)).(let H_x \def (aprem_gen_sort b2
+i h2 n2 H1) in (let H2 \def H_x in (False_ind (ex2 A (\lambda (b1: A).(leq g
+b1 b2)) (\lambda (b1: A).(aprem i (ASort h1 n1) b1))) H2)))))))))))) (\lambda
+(a0: A).(\lambda (a3: A).(\lambda (H0: (leq g a0 a3)).(\lambda (_: ((\forall
+(i: nat).(\forall (b2: A).((aprem i a3 b2) \to (ex2 A (\lambda (b1: A).(leq g
+b1 b2)) (\lambda (b1: A).(aprem i a0 b1)))))))).(\lambda (a4: A).(\lambda
+(a5: A).(\lambda (_: (leq g a4 a5)).(\lambda (H3: ((\forall (i: nat).(\forall
+(b2: A).((aprem i a5 b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda
+(b1: A).(aprem i a4 b1)))))))).(\lambda (i: nat).(\lambda (b2: A).(\lambda
+(H4: (aprem i (AHead a3 a5) b2)).(nat_ind (\lambda (n: nat).((aprem n (AHead
+a3 a5) b2) \to (ex2 A (\lambda (b1: A).(leq g b1 b2)) (\lambda (b1: A).(aprem
+n (AHead a0 a4) b1))))) (\lambda (H5: (aprem O (AHead a3 a5) b2)).(let H_y
+\def (aprem_gen_head_O a3 a5 b2 H5) in (eq_ind_r A a3 (\lambda (a: A).(ex2 A
+(\lambda (b1: A).(leq g b1 a)) (\lambda (b1: A).(aprem O (AHead a0 a4) b1))))