- \lambda (g: G).(\lambda (a1: A).(let TMP_1 \def (\lambda (a: A).(\forall
-(a2: A).((leq g (asucc g a) (asucc g a2)) \to (leq g a a2)))) in (let TMP_315
-\def (\lambda (n: nat).(\lambda (n0: nat).(\lambda (a2: A).(let TMP_3 \def
-(\lambda (a: A).((leq g (asucc g (ASort n n0)) (asucc g a)) \to (let TMP_2
-\def (ASort n n0) in (leq g TMP_2 a)))) in (let TMP_260 \def (\lambda (n1:
-nat).(\lambda (n2: nat).(\lambda (H: (leq g (asucc g (ASort n n0)) (asucc g
-(ASort n1 n2)))).(let TMP_6 \def (\lambda (n3: nat).((leq g (asucc g (ASort
-n3 n0)) (asucc g (ASort n1 n2))) \to (let TMP_4 \def (ASort n3 n0) in (let
-TMP_5 \def (ASort n1 n2) in (leq g TMP_4 TMP_5))))) in (let TMP_133 \def
-(\lambda (H0: (leq g (asucc g (ASort O n0)) (asucc g (ASort n1 n2)))).(let
-TMP_9 \def (\lambda (n3: nat).((leq g (asucc g (ASort O n0)) (asucc g (ASort
-n3 n2))) \to (let TMP_7 \def (ASort O n0) in (let TMP_8 \def (ASort n3 n2) in
-(leq g TMP_7 TMP_8))))) in (let TMP_73 \def (\lambda (H1: (leq g (asucc g
-(ASort O n0)) (asucc g (ASort O n2)))).(let TMP_10 \def (next g n0) in (let
-TMP_11 \def (next g n2) in (let TMP_12 \def (ASort O TMP_11) in (let H_x \def
-(leq_gen_sort1 g O TMP_10 TMP_12 H1) in (let H2 \def H_x in (let TMP_18 \def
-(\lambda (n3: nat).(\lambda (h2: nat).(\lambda (k: nat).(let TMP_13 \def
-(next g n0) in (let TMP_14 \def (ASort O TMP_13) in (let TMP_15 \def (aplus g
-TMP_14 k) in (let TMP_16 \def (ASort h2 n3) in (let TMP_17 \def (aplus g
-TMP_16 k) in (eq A TMP_15 TMP_17))))))))) in (let TMP_22 \def (\lambda (n3:
-nat).(\lambda (h2: nat).(\lambda (_: nat).(let TMP_19 \def (next g n2) in
-(let TMP_20 \def (ASort O TMP_19) in (let TMP_21 \def (ASort h2 n3) in (eq A
-TMP_20 TMP_21))))))) in (let TMP_23 \def (ASort O n0) in (let TMP_24 \def
-(ASort O n2) in (let TMP_25 \def (leq g TMP_23 TMP_24) in (let TMP_72 \def
-(\lambda (x0: nat).(\lambda (x1: nat).(\lambda (x2: nat).(\lambda (H3: (eq A
-(aplus g (ASort O (next g n0)) x2) (aplus g (ASort x1 x0) x2))).(\lambda (H4:
-(eq A (ASort O (next g n2)) (ASort x1 x0))).(let TMP_26 \def (\lambda (e:
-A).(match e with [(ASort n3 _) \Rightarrow n3 | (AHead _ _) \Rightarrow O]))
-in (let TMP_27 \def (next g n2) in (let TMP_28 \def (ASort O TMP_27) in (let
-TMP_29 \def (ASort x1 x0) in (let H5 \def (f_equal A nat TMP_26 TMP_28 TMP_29
-H4) in (let TMP_31 \def (\lambda (e: A).(match e with [(ASort _ n3)
-\Rightarrow n3 | (AHead _ _) \Rightarrow (let TMP_30 \def (match g with
-[(mk_G next _) \Rightarrow next]) in (TMP_30 n2))])) in (let TMP_32 \def
-(next g n2) in (let TMP_33 \def (ASort O TMP_32) in (let TMP_34 \def (ASort
-x1 x0) in (let H6 \def (f_equal A nat TMP_31 TMP_33 TMP_34 H4) in (let TMP_71
-\def (\lambda (H7: (eq nat O x1)).(let TMP_40 \def (\lambda (n3: nat).(let
-TMP_35 \def (next g n0) in (let TMP_36 \def (ASort O TMP_35) in (let TMP_37
-\def (aplus g TMP_36 x2) in (let TMP_38 \def (ASort n3 x0) in (let TMP_39
-\def (aplus g TMP_38 x2) in (eq A TMP_37 TMP_39))))))) in (let H8 \def
-(eq_ind_r nat x1 TMP_40 H3 O H7) in (let TMP_46 \def (\lambda (n3: nat).(let
-TMP_41 \def (next g n0) in (let TMP_42 \def (ASort O TMP_41) in (let TMP_43
-\def (aplus g TMP_42 x2) in (let TMP_44 \def (ASort O n3) in (let TMP_45 \def
-(aplus g TMP_44 x2) in (eq A TMP_43 TMP_45))))))) in (let TMP_47 \def (next g
-n2) in (let H9 \def (eq_ind_r nat x0 TMP_46 H8 TMP_47 H6) in (let TMP_48 \def
-(next g n0) in (let TMP_49 \def (ASort O TMP_48) in (let TMP_50 \def (aplus g
-TMP_49 x2) in (let TMP_54 \def (\lambda (a: A).(let TMP_51 \def (next g n2)
-in (let TMP_52 \def (ASort O TMP_51) in (let TMP_53 \def (aplus g TMP_52 x2)
-in (eq A a TMP_53))))) in (let TMP_55 \def (ASort O n0) in (let TMP_56 \def
-(S x2) in (let TMP_57 \def (aplus g TMP_55 TMP_56) in (let TMP_58 \def
-(aplus_sort_O_S_simpl g n0 x2) in (let H10 \def (eq_ind_r A TMP_50 TMP_54 H9
-TMP_57 TMP_58) in (let TMP_59 \def (next g n2) in (let TMP_60 \def (ASort O
-TMP_59) in (let TMP_61 \def (aplus g TMP_60 x2) in (let TMP_65 \def (\lambda
-(a: A).(let TMP_62 \def (ASort O n0) in (let TMP_63 \def (S x2) in (let
-TMP_64 \def (aplus g TMP_62 TMP_63) in (eq A TMP_64 a))))) in (let TMP_66
-\def (ASort O n2) in (let TMP_67 \def (S x2) in (let TMP_68 \def (aplus g
-TMP_66 TMP_67) in (let TMP_69 \def (aplus_sort_O_S_simpl g n2 x2) in (let H11
-\def (eq_ind_r A TMP_61 TMP_65 H10 TMP_68 TMP_69) in (let TMP_70 \def (S x2)
-in (leq_sort g O O n0 n2 TMP_70 H11)))))))))))))))))))))))))) in (TMP_71
-H5))))))))))))))))) in (ex2_3_ind nat nat nat TMP_18 TMP_22 TMP_25 TMP_72
-H2))))))))))))) in (let TMP_132 \def (\lambda (n3: nat).(\lambda (_: (((leq g
-(asucc g (ASort O n0)) (asucc g (ASort n3 n2))) \to (leq g (ASort O n0)
-(ASort n3 n2))))).(\lambda (H1: (leq g (asucc g (ASort O n0)) (asucc g (ASort
-(S n3) n2)))).(let TMP_74 \def (next g n0) in (let TMP_75 \def (ASort n3 n2)
-in (let H_x \def (leq_gen_sort1 g O TMP_74 TMP_75 H1) in (let H2 \def H_x in
-(let TMP_81 \def (\lambda (n4: nat).(\lambda (h2: nat).(\lambda (k: nat).(let
-TMP_76 \def (next g n0) in (let TMP_77 \def (ASort O TMP_76) in (let TMP_78
-\def (aplus g TMP_77 k) in (let TMP_79 \def (ASort h2 n4) in (let TMP_80 \def
-(aplus g TMP_79 k) in (eq A TMP_78 TMP_80))))))))) in (let TMP_84 \def
-(\lambda (n4: nat).(\lambda (h2: nat).(\lambda (_: nat).(let TMP_82 \def
-(ASort n3 n2) in (let TMP_83 \def (ASort h2 n4) in (eq A TMP_82 TMP_83))))))
-in (let TMP_85 \def (ASort O n0) in (let TMP_86 \def (S n3) in (let TMP_87
-\def (ASort TMP_86 n2) in (let TMP_88 \def (leq g TMP_85 TMP_87) in (let
-TMP_131 \def (\lambda (x0: nat).(\lambda (x1: nat).(\lambda (x2:
-nat).(\lambda (H3: (eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort
-x1 x0) x2))).(\lambda (H4: (eq A (ASort n3 n2) (ASort x1 x0))).(let TMP_89
-\def (\lambda (e: A).(match e with [(ASort n4 _) \Rightarrow n4 | (AHead _ _)
-\Rightarrow n3])) in (let TMP_90 \def (ASort n3 n2) in (let TMP_91 \def
-(ASort x1 x0) in (let H5 \def (f_equal A nat TMP_89 TMP_90 TMP_91 H4) in (let
-TMP_92 \def (\lambda (e: A).(match e with [(ASort _ n4) \Rightarrow n4 |
-(AHead _ _) \Rightarrow n2])) in (let TMP_93 \def (ASort n3 n2) in (let
-TMP_94 \def (ASort x1 x0) in (let H6 \def (f_equal A nat TMP_92 TMP_93 TMP_94
-H4) in (let TMP_130 \def (\lambda (H7: (eq nat n3 x1)).(let TMP_100 \def
-(\lambda (n4: nat).(let TMP_95 \def (next g n0) in (let TMP_96 \def (ASort O
-TMP_95) in (let TMP_97 \def (aplus g TMP_96 x2) in (let TMP_98 \def (ASort n4
-x0) in (let TMP_99 \def (aplus g TMP_98 x2) in (eq A TMP_97 TMP_99))))))) in
-(let H8 \def (eq_ind_r nat x1 TMP_100 H3 n3 H7) in (let TMP_106 \def (\lambda
-(n4: nat).(let TMP_101 \def (next g n0) in (let TMP_102 \def (ASort O
-TMP_101) in (let TMP_103 \def (aplus g TMP_102 x2) in (let TMP_104 \def
-(ASort n3 n4) in (let TMP_105 \def (aplus g TMP_104 x2) in (eq A TMP_103
-TMP_105))))))) in (let H9 \def (eq_ind_r nat x0 TMP_106 H8 n2 H6) in (let
-TMP_107 \def (next g n0) in (let TMP_108 \def (ASort O TMP_107) in (let
-TMP_109 \def (aplus g TMP_108 x2) in (let TMP_112 \def (\lambda (a: A).(let
-TMP_110 \def (ASort n3 n2) in (let TMP_111 \def (aplus g TMP_110 x2) in (eq A
-a TMP_111)))) in (let TMP_113 \def (ASort O n0) in (let TMP_114 \def (S x2)
-in (let TMP_115 \def (aplus g TMP_113 TMP_114) in (let TMP_116 \def
-(aplus_sort_O_S_simpl g n0 x2) in (let H10 \def (eq_ind_r A TMP_109 TMP_112
-H9 TMP_115 TMP_116) in (let TMP_117 \def (ASort n3 n2) in (let TMP_118 \def
-(aplus g TMP_117 x2) in (let TMP_122 \def (\lambda (a: A).(let TMP_119 \def
-(ASort O n0) in (let TMP_120 \def (S x2) in (let TMP_121 \def (aplus g
-TMP_119 TMP_120) in (eq A TMP_121 a))))) in (let TMP_123 \def (S n3) in (let
-TMP_124 \def (ASort TMP_123 n2) in (let TMP_125 \def (S x2) in (let TMP_126
-\def (aplus g TMP_124 TMP_125) in (let TMP_127 \def (aplus_sort_S_S_simpl g
-n2 n3 x2) in (let H11 \def (eq_ind_r A TMP_118 TMP_122 H10 TMP_126 TMP_127)
-in (let TMP_128 \def (S n3) in (let TMP_129 \def (S x2) in (leq_sort g O
-TMP_128 n0 n2 TMP_129 H11)))))))))))))))))))))))))) in (TMP_130
-H5))))))))))))))) in (ex2_3_ind nat nat nat TMP_81 TMP_84 TMP_88 TMP_131
-H2))))))))))))))) in (nat_ind TMP_9 TMP_73 TMP_132 n1 H0))))) in (let TMP_259
-\def (\lambda (n3: nat).(\lambda (IHn: (((leq g (asucc g (ASort n3 n0))
-(asucc g (ASort n1 n2))) \to (leq g (ASort n3 n0) (ASort n1 n2))))).(\lambda
-(H0: (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort n1 n2)))).(let
-TMP_137 \def (\lambda (n4: nat).((leq g (asucc g (ASort (S n3) n0)) (asucc g
-(ASort n4 n2))) \to ((((leq g (asucc g (ASort n3 n0)) (asucc g (ASort n4
-n2))) \to (leq g (ASort n3 n0) (ASort n4 n2)))) \to (let TMP_134 \def (S n3)
-in (let TMP_135 \def (ASort TMP_134 n0) in (let TMP_136 \def (ASort n4 n2) in
-(leq g TMP_135 TMP_136))))))) in (let TMP_200 \def (\lambda (H1: (leq g
-(asucc g (ASort (S n3) n0)) (asucc g (ASort O n2)))).(\lambda (_: (((leq g
-(asucc g (ASort n3 n0)) (asucc g (ASort O n2))) \to (leq g (ASort n3 n0)
-(ASort O n2))))).(let TMP_138 \def (next g n2) in (let TMP_139 \def (ASort O
-TMP_138) in (let H_x \def (leq_gen_sort1 g n3 n0 TMP_139 H1) in (let H2 \def
-H_x in (let TMP_144 \def (\lambda (n4: nat).(\lambda (h2: nat).(\lambda (k:
-nat).(let TMP_140 \def (ASort n3 n0) in (let TMP_141 \def (aplus g TMP_140 k)
-in (let TMP_142 \def (ASort h2 n4) in (let TMP_143 \def (aplus g TMP_142 k)
-in (eq A TMP_141 TMP_143)))))))) in (let TMP_148 \def (\lambda (n4:
-nat).(\lambda (h2: nat).(\lambda (_: nat).(let TMP_145 \def (next g n2) in
-(let TMP_146 \def (ASort O TMP_145) in (let TMP_147 \def (ASort h2 n4) in (eq
-A TMP_146 TMP_147))))))) in (let TMP_149 \def (S n3) in (let TMP_150 \def
-(ASort TMP_149 n0) in (let TMP_151 \def (ASort O n2) in (let TMP_152 \def
-(leq g TMP_150 TMP_151) in (let TMP_199 \def (\lambda (x0: nat).(\lambda (x1:
+ \lambda (g: G).(\lambda (a1: A).(A_ind (\lambda (a: A).(\forall (a2:
+A).((leq g (asucc g a) (asucc g a2)) \to (leq g a a2)))) (\lambda (n:
+nat).(\lambda (n0: nat).(\lambda (a2: A).(A_ind (\lambda (a: A).((leq g
+(asucc g (ASort n n0)) (asucc g a)) \to (leq g (ASort n n0) a))) (\lambda
+(n1: nat).(\lambda (n2: nat).(\lambda (H: (leq g (asucc g (ASort n n0))
+(asucc g (ASort n1 n2)))).(nat_ind (\lambda (n3: nat).((leq g (asucc g (ASort
+n3 n0)) (asucc g (ASort n1 n2))) \to (leq g (ASort n3 n0) (ASort n1 n2))))
+(\lambda (H0: (leq g (asucc g (ASort O n0)) (asucc g (ASort n1
+n2)))).(nat_ind (\lambda (n3: nat).((leq g (asucc g (ASort O n0)) (asucc g
+(ASort n3 n2))) \to (leq g (ASort O n0) (ASort n3 n2)))) (\lambda (H1: (leq g
+(asucc g (ASort O n0)) (asucc g (ASort O n2)))).(let H_x \def (leq_gen_sort1
+g O (next g n0) (ASort O (next g n2)) H1) in (let H2 \def H_x in (ex2_3_ind
+nat nat nat (\lambda (n3: nat).(\lambda (h2: nat).(\lambda (k: nat).(eq A
+(aplus g (ASort O (next g n0)) k) (aplus g (ASort h2 n3) k))))) (\lambda (n3:
+nat).(\lambda (h2: nat).(\lambda (_: nat).(eq A (ASort O (next g n2)) (ASort
+h2 n3))))) (leq g (ASort O n0) (ASort O n2)) (\lambda (x0: nat).(\lambda (x1:
+nat).(\lambda (x2: nat).(\lambda (H3: (eq A (aplus g (ASort O (next g n0))
+x2) (aplus g (ASort x1 x0) x2))).(\lambda (H4: (eq A (ASort O (next g n2))
+(ASort x1 x0))).(let H5 \def (f_equal A nat (\lambda (e: A).(match e with
+[(ASort n3 _) \Rightarrow n3 | (AHead _ _) \Rightarrow O])) (ASort O (next g
+n2)) (ASort x1 x0) H4) in ((let H6 \def (f_equal A nat (\lambda (e: A).(match
+e with [(ASort _ n3) \Rightarrow n3 | (AHead _ _) \Rightarrow ((match g with
+[(mk_G next _) \Rightarrow next]) n2)])) (ASort O (next g n2)) (ASort x1 x0)
+H4) in (\lambda (H7: (eq nat O x1)).(let H8 \def (eq_ind_r nat x1 (\lambda
+(n3: nat).(eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort n3 x0)
+x2))) H3 O H7) in (let H9 \def (eq_ind_r nat x0 (\lambda (n3: nat).(eq A
+(aplus g (ASort O (next g n0)) x2) (aplus g (ASort O n3) x2))) H8 (next g n2)
+H6) in (let H10 \def (eq_ind_r A (aplus g (ASort O (next g n0)) x2) (\lambda
+(a: A).(eq A a (aplus g (ASort O (next g n2)) x2))) H9 (aplus g (ASort O n0)
+(S x2)) (aplus_sort_O_S_simpl g n0 x2)) in (let H11 \def (eq_ind_r A (aplus g
+(ASort O (next g n2)) x2) (\lambda (a: A).(eq A (aplus g (ASort O n0) (S x2))
+a)) H10 (aplus g (ASort O n2) (S x2)) (aplus_sort_O_S_simpl g n2 x2)) in
+(leq_sort g O O n0 n2 (S x2) H11))))))) H5))))))) H2)))) (\lambda (n3:
+nat).(\lambda (_: (((leq g (asucc g (ASort O n0)) (asucc g (ASort n3 n2)))
+\to (leq g (ASort O n0) (ASort n3 n2))))).(\lambda (H1: (leq g (asucc g
+(ASort O n0)) (asucc g (ASort (S n3) n2)))).(let H_x \def (leq_gen_sort1 g O
+(next g n0) (ASort n3 n2) H1) in (let H2 \def H_x in (ex2_3_ind nat nat nat
+(\lambda (n4: nat).(\lambda (h2: nat).(\lambda (k: nat).(eq A (aplus g (ASort
+O (next g n0)) k) (aplus g (ASort h2 n4) k))))) (\lambda (n4: nat).(\lambda
+(h2: nat).(\lambda (_: nat).(eq A (ASort n3 n2) (ASort h2 n4))))) (leq g
+(ASort O n0) (ASort (S n3) n2)) (\lambda (x0: nat).(\lambda (x1:
+nat).(\lambda (x2: nat).(\lambda (H3: (eq A (aplus g (ASort O (next g n0))
+x2) (aplus g (ASort x1 x0) x2))).(\lambda (H4: (eq A (ASort n3 n2) (ASort x1
+x0))).(let H5 \def (f_equal A nat (\lambda (e: A).(match e with [(ASort n4 _)
+\Rightarrow n4 | (AHead _ _) \Rightarrow n3])) (ASort n3 n2) (ASort x1 x0)
+H4) in ((let H6 \def (f_equal A nat (\lambda (e: A).(match e with [(ASort _
+n4) \Rightarrow n4 | (AHead _ _) \Rightarrow n2])) (ASort n3 n2) (ASort x1
+x0) H4) in (\lambda (H7: (eq nat n3 x1)).(let H8 \def (eq_ind_r nat x1
+(\lambda (n4: nat).(eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort
+n4 x0) x2))) H3 n3 H7) in (let H9 \def (eq_ind_r nat x0 (\lambda (n4:
+nat).(eq A (aplus g (ASort O (next g n0)) x2) (aplus g (ASort n3 n4) x2))) H8
+n2 H6) in (let H10 \def (eq_ind_r A (aplus g (ASort O (next g n0)) x2)
+(\lambda (a: A).(eq A a (aplus g (ASort n3 n2) x2))) H9 (aplus g (ASort O n0)
+(S x2)) (aplus_sort_O_S_simpl g n0 x2)) in (let H11 \def (eq_ind_r A (aplus g
+(ASort n3 n2) x2) (\lambda (a: A).(eq A (aplus g (ASort O n0) (S x2)) a)) H10
+(aplus g (ASort (S n3) n2) (S x2)) (aplus_sort_S_S_simpl g n2 n3 x2)) in
+(leq_sort g O (S n3) n0 n2 (S x2) H11))))))) H5))))))) H2)))))) n1 H0))
+(\lambda (n3: nat).(\lambda (IHn: (((leq g (asucc g (ASort n3 n0)) (asucc g
+(ASort n1 n2))) \to (leq g (ASort n3 n0) (ASort n1 n2))))).(\lambda (H0: (leq
+g (asucc g (ASort (S n3) n0)) (asucc g (ASort n1 n2)))).(nat_ind (\lambda
+(n4: nat).((leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort n4 n2))) \to
+((((leq g (asucc g (ASort n3 n0)) (asucc g (ASort n4 n2))) \to (leq g (ASort
+n3 n0) (ASort n4 n2)))) \to (leq g (ASort (S n3) n0) (ASort n4 n2)))))
+(\lambda (H1: (leq g (asucc g (ASort (S n3) n0)) (asucc g (ASort O
+n2)))).(\lambda (_: (((leq g (asucc g (ASort n3 n0)) (asucc g (ASort O n2)))
+\to (leq g (ASort n3 n0) (ASort O n2))))).(let H_x \def (leq_gen_sort1 g n3
+n0 (ASort O (next g n2)) H1) in (let H2 \def H_x in (ex2_3_ind nat nat nat
+(\lambda (n4: nat).(\lambda (h2: nat).(\lambda (k: nat).(eq A (aplus g (ASort
+n3 n0) k) (aplus g (ASort h2 n4) k))))) (\lambda (n4: nat).(\lambda (h2:
+nat).(\lambda (_: nat).(eq A (ASort O (next g n2)) (ASort h2 n4))))) (leq g
+(ASort (S n3) n0) (ASort O n2)) (\lambda (x0: nat).(\lambda (x1: