-T).(ty3 g d1 u t))) (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))))).(let
-TMP_162 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let
-TMP_165 \def (\lambda (d2: C).(\lambda (u: T).(let TMP_163 \def (Bind Abbr)
-in (let TMP_164 \def (CHead d2 TMP_163 u) in (drop n O c2 TMP_164))))) in
-(let TMP_166 \def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) in (let
-TMP_167 \def (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) in (let
-TMP_168 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_171 \def (\lambda
-(d2: C).(let TMP_169 \def (Bind Abst) in (let TMP_170 \def (CHead d2 TMP_169
-t) in (getl n c2 TMP_170)))) in (let TMP_172 \def (ex2 C TMP_168 TMP_171) in
-(let TMP_173 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let
-TMP_176 \def (\lambda (d2: C).(\lambda (u: T).(let TMP_174 \def (Bind Abbr)
-in (let TMP_175 \def (CHead d2 TMP_174 u) in (getl n c2 TMP_175))))) in (let
-TMP_177 \def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_178
-\def (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_179 \def
-(ex4_2 C T TMP_173 TMP_176 TMP_177 TMP_178) in (let TMP_180 \def (or TMP_172
-TMP_179) in (let TMP_206 \def (\lambda (x1: C).(\lambda (x2: T).(\lambda
-(H17: (csubt g d1 x1)).(\lambda (H18: (drop n O c2 (CHead x1 (Bind Abbr)
-x2))).(\lambda (H19: (ty3 g d1 x2 t)).(\lambda (H20: (ty3 g x1 x2 t)).(let
-TMP_181 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_184 \def (\lambda
-(d2: C).(let TMP_182 \def (Bind Abst) in (let TMP_183 \def (CHead d2 TMP_182
-t) in (getl n c2 TMP_183)))) in (let TMP_185 \def (ex2 C TMP_181 TMP_184) in
-(let TMP_186 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let
-TMP_189 \def (\lambda (d2: C).(\lambda (u: T).(let TMP_187 \def (Bind Abbr)
-in (let TMP_188 \def (CHead d2 TMP_187 u) in (getl n c2 TMP_188))))) in (let
-TMP_190 \def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_191
-\def (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_192 \def
-(ex4_2 C T TMP_186 TMP_189 TMP_190 TMP_191) in (let TMP_193 \def (\lambda
-(d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_196 \def (\lambda (d2:
-C).(\lambda (u: T).(let TMP_194 \def (Bind Abbr) in (let TMP_195 \def (CHead
-d2 TMP_194 u) in (getl n c2 TMP_195))))) in (let TMP_197 \def (\lambda (_:
-C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_198 \def (\lambda (d2:
-C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_199 \def (Bind Abbr) in (let
-TMP_200 \def (CHead x1 TMP_199 x2) in (let TMP_201 \def (Bind Abbr) in (let
-TMP_202 \def (CHead x1 TMP_201 x2) in (let TMP_203 \def (clear_bind Abbr x1
-x2) in (let TMP_204 \def (getl_intro n c2 TMP_200 TMP_202 H18 TMP_203) in
-(let TMP_205 \def (ex4_2_intro C T TMP_193 TMP_196 TMP_197 TMP_198 x1 x2 H17
-TMP_204 H19 H20) in (or_intror TMP_185 TMP_192
-TMP_205)))))))))))))))))))))))))) in (ex4_2_ind C T TMP_162 TMP_165 TMP_166
-TMP_167 TMP_180 TMP_206 H16)))))))))))))))) in (let TMP_208 \def
-(csubt_drop_abst g n c1 c2 H12 d1 t H15) in (or_ind TMP_99 TMP_106 TMP_119
-TMP_161 TMP_207 TMP_208))))))))))))))))))))))))))))))) in (let TMP_210 \def
-(TMP_209 H8) in (TMP_210 H7))))))))))))))))))))))))))))))))) in (let TMP_577
-\def (\lambda (f: F).(\lambda (H5: (drop n O c1 (CHead x0 (Flat f)
-t0))).(\lambda (H6: (clear (CHead x0 (Flat f) t0) (CHead d1 (Bind Abst)
-t))).(let H7 \def H5 in (let TMP_224 \def (\lambda (c: C).((drop n O c (CHead
-x0 (Flat f) t0)) \to (\forall (c2: C).((csubt g c c2) \to (let TMP_212 \def
-(\lambda (d2: C).(csubt g d1 d2)) in (let TMP_215 \def (\lambda (d2: C).(let
-TMP_213 \def (Bind Abst) in (let TMP_214 \def (CHead d2 TMP_213 t) in (getl n
-c2 TMP_214)))) in (let TMP_216 \def (ex2 C TMP_212 TMP_215) in (let TMP_217
-\def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_220 \def
-(\lambda (d2: C).(\lambda (u: T).(let TMP_218 \def (Bind Abbr) in (let
-TMP_219 \def (CHead d2 TMP_218 u) in (getl n c2 TMP_219))))) in (let TMP_221
-\def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_222 \def
-(\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_223 \def (ex4_2
-C T TMP_217 TMP_220 TMP_221 TMP_222) in (or TMP_216 TMP_223))))))))))))) in
-(let TMP_237 \def (\lambda (n0: nat).(\forall (x1: C).((drop n0 O x1 (CHead
-x0 (Flat f) t0)) \to (\forall (c2: C).((csubt g x1 c2) \to (let TMP_225 \def
-(\lambda (d2: C).(csubt g d1 d2)) in (let TMP_228 \def (\lambda (d2: C).(let
-TMP_226 \def (Bind Abst) in (let TMP_227 \def (CHead d2 TMP_226 t) in (getl
-n0 c2 TMP_227)))) in (let TMP_229 \def (ex2 C TMP_225 TMP_228) in (let
-TMP_230 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let
-TMP_233 \def (\lambda (d2: C).(\lambda (u: T).(let TMP_231 \def (Bind Abbr)
-in (let TMP_232 \def (CHead d2 TMP_231 u) in (getl n0 c2 TMP_232))))) in (let
-TMP_234 \def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_235
-\def (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_236 \def
-(ex4_2 C T TMP_230 TMP_233 TMP_234 TMP_235) in (or TMP_229
-TMP_236)))))))))))))) in (let TMP_386 \def (\lambda (x1: C).(\lambda (H8:
-(drop O O x1 (CHead x0 (Flat f) t0))).(\lambda (c2: C).(\lambda (H9: (csubt g
-x1 c2)).(let TMP_238 \def (\lambda (c: C).(csubt g c c2)) in (let TMP_239
-\def (Flat f) in (let TMP_240 \def (CHead x0 TMP_239 t0) in (let TMP_241 \def
-(Flat f) in (let TMP_242 \def (CHead x0 TMP_241 t0) in (let TMP_243 \def
-(drop_gen_refl x1 TMP_242 H8) in (let H10 \def (eq_ind C x1 TMP_238 H9
-TMP_240 TMP_243) in (let TMP_244 \def (Bind Abst) in (let TMP_245 \def (CHead
-d1 TMP_244 t) in (let TMP_246 \def (Bind Abst) in (let TMP_247 \def (CHead d1
-TMP_246 t) in (let TMP_248 \def (clear_gen_flat f x0 TMP_247 t0 H6) in (let
-H_y \def (clear_flat x0 TMP_245 TMP_248 f t0) in (let TMP_249 \def (Flat f)
-in (let TMP_250 \def (CHead x0 TMP_249 t0) in (let TMP_251 \def (Bind Abst)
-in (let TMP_252 \def (CHead d1 TMP_251 t) in (let H11 \def (csubt_clear_conf
-g TMP_250 c2 H10 TMP_252 H_y) in (let TMP_255 \def (\lambda (e2: C).(let
-TMP_253 \def (Bind Abst) in (let TMP_254 \def (CHead d1 TMP_253 t) in (csubt
-g TMP_254 e2)))) in (let TMP_256 \def (\lambda (e2: C).(clear c2 e2)) in (let
-TMP_257 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_260 \def (\lambda
-(d2: C).(let TMP_258 \def (Bind Abst) in (let TMP_259 \def (CHead d2 TMP_258
-t) in (getl O c2 TMP_259)))) in (let TMP_261 \def (ex2 C TMP_257 TMP_260) in
-(let TMP_262 \def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let
-TMP_265 \def (\lambda (d2: C).(\lambda (u: T).(let TMP_263 \def (Bind Abbr)
-in (let TMP_264 \def (CHead d2 TMP_263 u) in (getl O c2 TMP_264))))) in (let
-TMP_266 \def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_267
-\def (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_268 \def
-(ex4_2 C T TMP_262 TMP_265 TMP_266 TMP_267) in (let TMP_269 \def (or TMP_261
-TMP_268) in (let TMP_385 \def (\lambda (x2: C).(\lambda (H12: (csubt g (CHead
-d1 (Bind Abst) t) x2)).(\lambda (H13: (clear c2 x2)).(let H14 \def
-(csubt_gen_abst g d1 x2 t H12) in (let TMP_272 \def (\lambda (e2: C).(let
-TMP_270 \def (Bind Abst) in (let TMP_271 \def (CHead e2 TMP_270 t) in (eq C
-x2 TMP_271)))) in (let TMP_273 \def (\lambda (e2: C).(csubt g d1 e2)) in (let
-TMP_274 \def (ex2 C TMP_272 TMP_273) in (let TMP_277 \def (\lambda (e2:
-C).(\lambda (v2: T).(let TMP_275 \def (Bind Abbr) in (let TMP_276 \def (CHead
-e2 TMP_275 v2) in (eq C x2 TMP_276))))) in (let TMP_278 \def (\lambda (e2:
-C).(\lambda (_: T).(csubt g d1 e2))) in (let TMP_279 \def (\lambda (_:
-C).(\lambda (v2: T).(ty3 g d1 v2 t))) in (let TMP_280 \def (\lambda (e2:
-C).(\lambda (v2: T).(ty3 g e2 v2 t))) in (let TMP_281 \def (ex4_2 C T TMP_277
-TMP_278 TMP_279 TMP_280) in (let TMP_282 \def (\lambda (d2: C).(csubt g d1
-d2)) in (let TMP_285 \def (\lambda (d2: C).(let TMP_283 \def (Bind Abst) in
-(let TMP_284 \def (CHead d2 TMP_283 t) in (getl O c2 TMP_284)))) in (let
-TMP_286 \def (ex2 C TMP_282 TMP_285) in (let TMP_287 \def (\lambda (d2:
-C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_290 \def (\lambda (d2:
-C).(\lambda (u: T).(let TMP_288 \def (Bind Abbr) in (let TMP_289 \def (CHead
-d2 TMP_288 u) in (getl O c2 TMP_289))))) in (let TMP_291 \def (\lambda (_:
-C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_292 \def (\lambda (d2:
-C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_293 \def (ex4_2 C T TMP_287
-TMP_290 TMP_291 TMP_292) in (let TMP_294 \def (or TMP_286 TMP_293) in (let
-TMP_337 \def (\lambda (H15: (ex2 C (\lambda (e2: C).(eq C x2 (CHead e2 (Bind
-Abst) t))) (\lambda (e2: C).(csubt g d1 e2)))).(let TMP_297 \def (\lambda
-(e2: C).(let TMP_295 \def (Bind Abst) in (let TMP_296 \def (CHead e2 TMP_295
-t) in (eq C x2 TMP_296)))) in (let TMP_298 \def (\lambda (e2: C).(csubt g d1
-e2)) in (let TMP_299 \def (\lambda (d2: C).(csubt g d1 d2)) in (let TMP_302
-\def (\lambda (d2: C).(let TMP_300 \def (Bind Abst) in (let TMP_301 \def
-(CHead d2 TMP_300 t) in (getl O c2 TMP_301)))) in (let TMP_303 \def (ex2 C
-TMP_299 TMP_302) in (let TMP_304 \def (\lambda (d2: C).(\lambda (_: T).(csubt
-g d1 d2))) in (let TMP_307 \def (\lambda (d2: C).(\lambda (u: T).(let TMP_305
-\def (Bind Abbr) in (let TMP_306 \def (CHead d2 TMP_305 u) in (getl O c2
-TMP_306))))) in (let TMP_308 \def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u
-t))) in (let TMP_309 \def (\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t)))
-in (let TMP_310 \def (ex4_2 C T TMP_304 TMP_307 TMP_308 TMP_309) in (let
-TMP_311 \def (or TMP_303 TMP_310) in (let TMP_336 \def (\lambda (x3:
-C).(\lambda (H16: (eq C x2 (CHead x3 (Bind Abst) t))).(\lambda (H17: (csubt g
-d1 x3)).(let TMP_312 \def (\lambda (c: C).(clear c2 c)) in (let TMP_313 \def
-(Bind Abst) in (let TMP_314 \def (CHead x3 TMP_313 t) in (let H18 \def
-(eq_ind C x2 TMP_312 H13 TMP_314 H16) in (let TMP_315 \def (\lambda (d2:
-C).(csubt g d1 d2)) in (let TMP_318 \def (\lambda (d2: C).(let TMP_316 \def
-(Bind Abst) in (let TMP_317 \def (CHead d2 TMP_316 t) in (getl O c2
-TMP_317)))) in (let TMP_319 \def (ex2 C TMP_315 TMP_318) in (let TMP_320 \def
-(\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_323 \def
-(\lambda (d2: C).(\lambda (u: T).(let TMP_321 \def (Bind Abbr) in (let
-TMP_322 \def (CHead d2 TMP_321 u) in (getl O c2 TMP_322))))) in (let TMP_324
-\def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_325 \def
-(\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_326 \def (ex4_2
-C T TMP_320 TMP_323 TMP_324 TMP_325) in (let TMP_327 \def (\lambda (d2:
-C).(csubt g d1 d2)) in (let TMP_330 \def (\lambda (d2: C).(let TMP_328 \def
-(Bind Abst) in (let TMP_329 \def (CHead d2 TMP_328 t) in (getl O c2
-TMP_329)))) in (let TMP_331 \def (Bind Abst) in (let TMP_332 \def (CHead x3
-TMP_331 t) in (let TMP_333 \def (drop_refl c2) in (let TMP_334 \def
-(getl_intro O c2 TMP_332 c2 TMP_333 H18) in (let TMP_335 \def (ex_intro2 C
-TMP_327 TMP_330 x3 H17 TMP_334) in (or_introl TMP_319 TMP_326
-TMP_335))))))))))))))))))))))) in (ex2_ind C TMP_297 TMP_298 TMP_311 TMP_336
-H15)))))))))))))) in (let TMP_384 \def (\lambda (H15: (ex4_2 C T (\lambda
-(e2: C).(\lambda (v2: T).(eq C x2 (CHead e2 (Bind Abbr) v2)))) (\lambda (e2:
-C).(\lambda (_: T).(csubt g d1 e2))) (\lambda (_: C).(\lambda (v2: T).(ty3 g
-d1 v2 t))) (\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 t))))).(let TMP_340
-\def (\lambda (e2: C).(\lambda (v2: T).(let TMP_338 \def (Bind Abbr) in (let
-TMP_339 \def (CHead e2 TMP_338 v2) in (eq C x2 TMP_339))))) in (let TMP_341
-\def (\lambda (e2: C).(\lambda (_: T).(csubt g d1 e2))) in (let TMP_342 \def
-(\lambda (_: C).(\lambda (v2: T).(ty3 g d1 v2 t))) in (let TMP_343 \def
-(\lambda (e2: C).(\lambda (v2: T).(ty3 g e2 v2 t))) in (let TMP_344 \def
-(\lambda (d2: C).(csubt g d1 d2)) in (let TMP_347 \def (\lambda (d2: C).(let
-TMP_345 \def (Bind Abst) in (let TMP_346 \def (CHead d2 TMP_345 t) in (getl O
-c2 TMP_346)))) in (let TMP_348 \def (ex2 C TMP_344 TMP_347) in (let TMP_349
-\def (\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_352 \def
-(\lambda (d2: C).(\lambda (u: T).(let TMP_350 \def (Bind Abbr) in (let
-TMP_351 \def (CHead d2 TMP_350 u) in (getl O c2 TMP_351))))) in (let TMP_353
-\def (\lambda (_: C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_354 \def
-(\lambda (d2: C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_355 \def (ex4_2
-C T TMP_349 TMP_352 TMP_353 TMP_354) in (let TMP_356 \def (or TMP_348
-TMP_355) in (let TMP_383 \def (\lambda (x3: C).(\lambda (x4: T).(\lambda
-(H16: (eq C x2 (CHead x3 (Bind Abbr) x4))).(\lambda (H17: (csubt g d1
-x3)).(\lambda (H18: (ty3 g d1 x4 t)).(\lambda (H19: (ty3 g x3 x4 t)).(let
-TMP_357 \def (\lambda (c: C).(clear c2 c)) in (let TMP_358 \def (Bind Abbr)
-in (let TMP_359 \def (CHead x3 TMP_358 x4) in (let H20 \def (eq_ind C x2
-TMP_357 H13 TMP_359 H16) in (let TMP_360 \def (\lambda (d2: C).(csubt g d1
-d2)) in (let TMP_363 \def (\lambda (d2: C).(let TMP_361 \def (Bind Abst) in
-(let TMP_362 \def (CHead d2 TMP_361 t) in (getl O c2 TMP_362)))) in (let
-TMP_364 \def (ex2 C TMP_360 TMP_363) in (let TMP_365 \def (\lambda (d2:
-C).(\lambda (_: T).(csubt g d1 d2))) in (let TMP_368 \def (\lambda (d2:
-C).(\lambda (u: T).(let TMP_366 \def (Bind Abbr) in (let TMP_367 \def (CHead
-d2 TMP_366 u) in (getl O c2 TMP_367))))) in (let TMP_369 \def (\lambda (_:
-C).(\lambda (u: T).(ty3 g d1 u t))) in (let TMP_370 \def (\lambda (d2:
-C).(\lambda (u: T).(ty3 g d2 u t))) in (let TMP_371 \def (ex4_2 C T TMP_365
-TMP_368 TMP_369 TMP_370) in (let TMP_372 \def (\lambda (d2: C).(\lambda (_:
-T).(csubt g d1 d2))) in (let TMP_375 \def (\lambda (d2: C).(\lambda (u:
-T).(let TMP_373 \def (Bind Abbr) in (let TMP_374 \def (CHead d2 TMP_373 u) in
-(getl O c2 TMP_374))))) in (let TMP_376 \def (\lambda (_: C).(\lambda (u:
-T).(ty3 g d1 u t))) in (let TMP_377 \def (\lambda (d2: C).(\lambda (u:
-T).(ty3 g d2 u t))) in (let TMP_378 \def (Bind Abbr) in (let TMP_379 \def
-(CHead x3 TMP_378 x4) in (let TMP_380 \def (drop_refl c2) in (let TMP_381
-\def (getl_intro O c2 TMP_379 c2 TMP_380 H20) in (let TMP_382 \def
-(ex4_2_intro C T TMP_372 TMP_375 TMP_376 TMP_377 x3 x4 H17 TMP_381 H18 H19)
-in (or_intror TMP_364 TMP_371 TMP_382)))))))))))))))))))))))))))) in
-(ex4_2_ind C T TMP_340 TMP_341 TMP_342 TMP_343 TMP_356 TMP_383
-H15)))))))))))))))) in (or_ind TMP_274 TMP_281 TMP_294 TMP_337 TMP_384
-H14)))))))))))))))))))))))) in (ex2_ind C TMP_255 TMP_256 TMP_269 TMP_385
-H11))))))))))))))))))))))))))))))))))) in (let TMP_575 \def (\lambda (n0:
-nat).(\lambda (H8: ((\forall (x1: C).((drop n0 O x1 (CHead x0 (Flat f) t0))
-\to (\forall (c2: C).((csubt g x1 c2) \to (or (ex2 C (\lambda (d2: C).(csubt
-g d1 d2)) (\lambda (d2: C).(getl n0 c2 (CHead d2 (Bind Abst) t)))) (ex4_2 C T
-(\lambda (d2: C).(\lambda (_: T).(csubt g d1 d2))) (\lambda (d2: C).(\lambda
-(u: T).(getl n0 c2 (CHead d2 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: