+b))))))))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity g c0 t0
+(AHead a1 a2))).(\lambda (H3: ((\forall (i: nat).(\forall (b: A).((aprem i
+(AHead a1 a2) b) \to (ex2_3 C T nat (\lambda (d: C).(\lambda (_: T).(\lambda
+(j: nat).(drop (plus i j) O d c0)))) (\lambda (d: C).(\lambda (u0:
+T).(\lambda (_: nat).(arity g d u0 (asucc g b))))))))))).(\lambda (i:
+nat).(\lambda (b: A).(\lambda (H4: (aprem i a2 b)).(let TMP_146 \def (S i) in
+(let H_y \def (H3 TMP_146 b) in (let TMP_147 \def (aprem_succ a2 b i H4 a1)
+in (let H5 \def (H_y TMP_147) in (let TMP_150 \def (\lambda (d: C).(\lambda
+(_: T).(\lambda (j: nat).(let TMP_148 \def (plus i j) in (let TMP_149 \def (S
+TMP_148) in (drop TMP_149 O d c0)))))) in (let TMP_152 \def (\lambda (d:
+C).(\lambda (u0: T).(\lambda (_: nat).(let TMP_151 \def (asucc g b) in (arity
+g d u0 TMP_151))))) in (let TMP_154 \def (\lambda (d: C).(\lambda (_:
+T).(\lambda (j: nat).(let TMP_153 \def (plus i j) in (drop TMP_153 O d
+c0))))) in (let TMP_156 \def (\lambda (d: C).(\lambda (u0: T).(\lambda (_:
+nat).(let TMP_155 \def (asucc g b) in (arity g d u0 TMP_155))))) in (let
+TMP_157 \def (ex2_3 C T nat TMP_154 TMP_156) in (let TMP_235 \def (\lambda
+(x0: C).(\lambda (x1: T).(\lambda (x2: nat).(\lambda (H6: (drop (S (plus i
+x2)) O x0 c0)).(\lambda (H7: (arity g x0 x1 (asucc g b))).(let TMP_162 \def
+(\lambda (c1: C).((drop (S (plus i x2)) O c1 c0) \to ((arity g c1 x1 (asucc g
+b)) \to (let TMP_159 \def (\lambda (d: C).(\lambda (_: T).(\lambda (j:
+nat).(let TMP_158 \def (plus i j) in (drop TMP_158 O d c0))))) in (let
+TMP_161 \def (\lambda (d: C).(\lambda (u0: T).(\lambda (_: nat).(let TMP_160
+\def (asucc g b) in (arity g d u0 TMP_160))))) in (ex2_3 C T nat TMP_159
+TMP_161)))))) in (let TMP_186 \def (\lambda (n: nat).(\lambda (H8: (drop (S
+(plus i x2)) O (CSort n) c0)).(\lambda (_: (arity g (CSort n) x1 (asucc g
+b))).(let TMP_163 \def (CSort n) in (let TMP_164 \def (eq C c0 TMP_163) in
+(let TMP_165 \def (plus i x2) in (let TMP_166 \def (S TMP_165) in (let
+TMP_167 \def (eq nat TMP_166 O) in (let TMP_168 \def (eq nat O O) in (let
+TMP_170 \def (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(let TMP_169
+\def (plus i j) in (drop TMP_169 O d c0))))) in (let TMP_172 \def (\lambda
+(d: C).(\lambda (u0: T).(\lambda (_: nat).(let TMP_171 \def (asucc g b) in
+(arity g d u0 TMP_171))))) in (let TMP_173 \def (ex2_3 C T nat TMP_170
+TMP_172) in (let TMP_182 \def (\lambda (_: (eq C c0 (CSort n))).(\lambda
+(H11: (eq nat (S (plus i x2)) O)).(\lambda (_: (eq nat O O)).(let TMP_174
+\def (plus i x2) in (let TMP_175 \def (S TMP_174) in (let TMP_176 \def
+(\lambda (ee: nat).(match ee with [O \Rightarrow False | (S _) \Rightarrow
+True])) in (let H13 \def (eq_ind nat TMP_175 TMP_176 I O H11) in (let TMP_178
+\def (\lambda (d: C).(\lambda (_: T).(\lambda (j: nat).(let TMP_177 \def
+(plus i j) in (drop TMP_177 O d c0))))) in (let TMP_180 \def (\lambda (d:
+C).(\lambda (u0: T).(\lambda (_: nat).(let TMP_179 \def (asucc g b) in (arity
+g d u0 TMP_179))))) in (let TMP_181 \def (ex2_3 C T nat TMP_178 TMP_180) in
+(False_ind TMP_181 H13))))))))))) in (let TMP_183 \def (plus i x2) in (let
+TMP_184 \def (S TMP_183) in (let TMP_185 \def (drop_gen_sort n TMP_184 O c0
+H8) in (and3_ind TMP_164 TMP_167 TMP_168 TMP_173 TMP_182
+TMP_185))))))))))))))))) in (let TMP_234 \def (\lambda (d: C).(\lambda (IHd:
+(((drop (S (plus i x2)) O d c0) \to ((arity g d x1 (asucc g b)) \to (ex2_3 C
+T nat (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(drop (plus i j) O
+d0 c0)))) (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(arity g d0 u0
+(asucc g b)))))))))).(\lambda (k: K).(\lambda (t1: T).(\lambda (H8: (drop (S
+(plus i x2)) O (CHead d k t1) c0)).(\lambda (H9: (arity g (CHead d k t1) x1
+(asucc g b))).(let TMP_191 \def (\lambda (k0: K).((arity g (CHead d k0 t1) x1
+(asucc g b)) \to ((drop (r k0 (plus i x2)) O d c0) \to (let TMP_188 \def
+(\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(let TMP_187 \def (plus i
+j) in (drop TMP_187 O d0 c0))))) in (let TMP_190 \def (\lambda (d0:
+C).(\lambda (u0: T).(\lambda (_: nat).(let TMP_189 \def (asucc g b) in (arity
+g d0 u0 TMP_189))))) in (ex2_3 C T nat TMP_188 TMP_190)))))) in (let TMP_211
+\def (\lambda (b0: B).(\lambda (H10: (arity g (CHead d (Bind b0) t1) x1
+(asucc g b))).(\lambda (H11: (drop (r (Bind b0) (plus i x2)) O d c0)).(let
+TMP_193 \def (\lambda (d0: C).(\lambda (_: T).(\lambda (j: nat).(let TMP_192
+\def (plus i j) in (drop TMP_192 O d0 c0))))) in (let TMP_195 \def (\lambda
+(d0: C).(\lambda (u0: T).(\lambda (_: nat).(let TMP_194 \def (asucc g b) in
+(arity g d0 u0 TMP_194))))) in (let TMP_196 \def (Bind b0) in (let TMP_197
+\def (CHead d TMP_196 t1) in (let TMP_198 \def (S x2) in (let TMP_199 \def
+(plus i x2) in (let TMP_200 \def (S TMP_199) in (let TMP_203 \def (\lambda
+(n: nat).(let TMP_201 \def (Bind b0) in (let TMP_202 \def (CHead d TMP_201
+t1) in (drop n O TMP_202 c0)))) in (let TMP_204 \def (Bind b0) in (let
+TMP_205 \def (plus i x2) in (let TMP_206 \def (drop_drop TMP_204 TMP_205 d c0
+H11 t1) in (let TMP_207 \def (S x2) in (let TMP_208 \def (plus i TMP_207) in
+(let TMP_209 \def (plus_n_Sm i x2) in (let TMP_210 \def (eq_ind nat TMP_200
+TMP_203 TMP_206 TMP_208 TMP_209) in (ex2_3_intro C T nat TMP_193 TMP_195
+TMP_197 x1 TMP_198 TMP_210 H10))))))))))))))))))) in (let TMP_231 \def
+(\lambda (f: F).(\lambda (H10: (arity g (CHead d (Flat f) t1) x1 (asucc g
+b))).(\lambda (H11: (drop (r (Flat f) (plus i x2)) O d c0)).(let TMP_212 \def
+(Flat f) in (let TMP_213 \def (CHead d TMP_212 t1) in (let TMP_214 \def
+(asucc g b) in (let TMP_215 \def (cimp_flat_sx f d t1) in (let TMP_216 \def
+(arity_cimp_conf g TMP_213 x1 TMP_214 H10 d TMP_215) in (let H12 \def (IHd
+H11 TMP_216) in (let TMP_218 \def (\lambda (d0: C).(\lambda (_: T).(\lambda
+(j: nat).(let TMP_217 \def (plus i j) in (drop TMP_217 O d0 c0))))) in (let
+TMP_220 \def (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(let TMP_219
+\def (asucc g b) in (arity g d0 u0 TMP_219))))) in (let TMP_222 \def (\lambda
+(d0: C).(\lambda (_: T).(\lambda (j: nat).(let TMP_221 \def (plus i j) in
+(drop TMP_221 O d0 c0))))) in (let TMP_224 \def (\lambda (d0: C).(\lambda
+(u0: T).(\lambda (_: nat).(let TMP_223 \def (asucc g b) in (arity g d0 u0
+TMP_223))))) in (let TMP_225 \def (ex2_3 C T nat TMP_222 TMP_224) in (let
+TMP_230 \def (\lambda (x3: C).(\lambda (x4: T).(\lambda (x5: nat).(\lambda
+(H13: (drop (plus i x5) O x3 c0)).(\lambda (H14: (arity g x3 x4 (asucc g
+b))).(let TMP_227 \def (\lambda (d0: C).(\lambda (_: T).(\lambda (j:
+nat).(let TMP_226 \def (plus i j) in (drop TMP_226 O d0 c0))))) in (let
+TMP_229 \def (\lambda (d0: C).(\lambda (u0: T).(\lambda (_: nat).(let TMP_228
+\def (asucc g b) in (arity g d0 u0 TMP_228))))) in (ex2_3_intro C T nat
+TMP_227 TMP_229 x3 x4 x5 H13 H14)))))))) in (ex2_3_ind C T nat TMP_218
+TMP_220 TMP_225 TMP_230 H12)))))))))))))))) in (let TMP_232 \def (plus i x2)
+in (let TMP_233 \def (drop_gen_drop k d c0 t1 TMP_232 H8) in (K_ind TMP_191
+TMP_211 TMP_231 k H9 TMP_233)))))))))))) in (C_ind TMP_162 TMP_186 TMP_234 x0
+H6 H7))))))))) in (ex2_3_ind C T nat TMP_150 TMP_152 TMP_157 TMP_235
+H5))))))))))))))))))))))) in (let TMP_251 \def (\lambda (c0: C).(\lambda (u:
+T).(\lambda (a0: A).(\lambda (_: (arity g c0 u (asucc g a0))).(\lambda (_:
+((\forall (i: nat).(\forall (b: A).((aprem i (asucc g a0) b) \to (ex2_3 C T