-Prop).P)))))).(\lambda (t2: T).(let TMP_333 \def (\lambda (t3: T).(let
-TMP_331 \def (THead k t t0) in (let TMP_332 \def (eq T TMP_331 t3) in (let
-TMP_330 \def ((eq T (THead k t t0) t3) \to (\forall (P: Prop).P)) in (or
-TMP_332 TMP_330))))) in (let TMP_329 \def (\lambda (n: nat).(let TMP_327 \def
-(THead k t t0) in (let TMP_326 \def (TSort n) in (let TMP_328 \def (eq T
-TMP_327 TMP_326) in (let TMP_325 \def ((eq T (THead k t t0) (TSort n)) \to
-(\forall (P: Prop).P)) in (let TMP_324 \def (\lambda (H1: (eq T (THead k t
-t0) (TSort n))).(\lambda (P: Prop).(let TMP_323 \def (THead k t t0) in (let
-TMP_322 \def (\lambda (ee: T).(match ee in T with [(TSort _) \Rightarrow
-False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) in
-(let TMP_321 \def (TSort n) in (let H2 \def (eq_ind T TMP_323 TMP_322 I
-TMP_321 H1) in (False_ind P H2))))))) in (or_intror TMP_328 TMP_325
-TMP_324))))))) in (let TMP_320 \def (\lambda (n: nat).(let TMP_318 \def
-(THead k t t0) in (let TMP_317 \def (TLRef n) in (let TMP_319 \def (eq T
-TMP_318 TMP_317) in (let TMP_316 \def ((eq T (THead k t t0) (TLRef n)) \to
-(\forall (P: Prop).P)) in (let TMP_315 \def (\lambda (H1: (eq T (THead k t
-t0) (TLRef n))).(\lambda (P: Prop).(let TMP_314 \def (THead k t t0) in (let
-TMP_313 \def (\lambda (ee: T).(match ee in T with [(TSort _) \Rightarrow
-False | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) in
-(let TMP_312 \def (TLRef n) in (let H2 \def (eq_ind T TMP_314 TMP_313 I
-TMP_312 H1) in (False_ind P H2))))))) in (or_intror TMP_319 TMP_316
-TMP_315))))))) in (let TMP_311 \def (\lambda (k0: K).(\lambda (t3:
-T).(\lambda (H1: (or (eq T (THead k t t0) t3) ((eq T (THead k t t0) t3) \to
-(\forall (P: Prop).P)))).(\lambda (t4: T).(\lambda (H2: (or (eq T (THead k t
-t0) t4) ((eq T (THead k t t0) t4) \to (\forall (P: Prop).P)))).(let H_x \def
-(H t3) in (let H3 \def H_x in (let TMP_310 \def (eq T t t3) in (let TMP_309
-\def ((eq T t t3) \to (\forall (P: Prop).P)) in (let TMP_306 \def (THead k t
-t0) in (let TMP_305 \def (THead k0 t3 t4) in (let TMP_307 \def (eq T TMP_306
-TMP_305) in (let TMP_304 \def ((eq T (THead k t t0) (THead k0 t3 t4)) \to
-(\forall (P: Prop).P)) in (let TMP_308 \def (or TMP_307 TMP_304) in (let
-TMP_303 \def (\lambda (H4: (eq T t t3)).(let TMP_228 \def (\lambda (t5:
-T).(let TMP_226 \def (THead k t t0) in (let TMP_227 \def (eq T TMP_226 t5) in
-(let TMP_225 \def ((eq T (THead k t t0) t5) \to (\forall (P: Prop).P)) in (or
-TMP_227 TMP_225))))) in (let H5 \def (eq_ind_r T t3 TMP_228 H1 t H4) in (let
-TMP_302 \def (\lambda (t5: T).(let TMP_300 \def (THead k t t0) in (let
-TMP_299 \def (THead k0 t5 t4) in (let TMP_301 \def (eq T TMP_300 TMP_299) in
-(let TMP_298 \def ((eq T (THead k t t0) (THead k0 t5 t4)) \to (\forall (P:
-Prop).P)) in (or TMP_301 TMP_298)))))) in (let H_x0 \def (H0 t4) in (let H6
-\def H_x0 in (let TMP_296 \def (eq T t0 t4) in (let TMP_295 \def ((eq T t0
-t4) \to (\forall (P: Prop).P)) in (let TMP_292 \def (THead k t t0) in (let
-TMP_291 \def (THead k0 t t4) in (let TMP_293 \def (eq T TMP_292 TMP_291) in
-(let TMP_290 \def ((eq T (THead k t t0) (THead k0 t t4)) \to (\forall (P:
-Prop).P)) in (let TMP_294 \def (or TMP_293 TMP_290) in (let TMP_289 \def
-(\lambda (H7: (eq T t0 t4)).(let TMP_251 \def (\lambda (t5: T).(let TMP_249
-\def (THead k t t0) in (let TMP_250 \def (eq T TMP_249 t5) in (let TMP_248
-\def ((eq T (THead k t t0) t5) \to (\forall (P: Prop).P)) in (or TMP_250
-TMP_248))))) in (let H8 \def (eq_ind_r T t4 TMP_251 H2 t0 H7) in (let TMP_288
-\def (\lambda (t5: T).(let TMP_286 \def (THead k t t0) in (let TMP_285 \def
-(THead k0 t t5) in (let TMP_287 \def (eq T TMP_286 TMP_285) in (let TMP_284
-\def ((eq T (THead k t t0) (THead k0 t t5)) \to (\forall (P: Prop).P)) in (or
-TMP_287 TMP_284)))))) in (let H_x1 \def (terms_props__kind_dec k k0) in (let
-H9 \def H_x1 in (let TMP_282 \def (eq K k k0) in (let TMP_281 \def ((eq K k
-k0) \to (\forall (P: Prop).P)) in (let TMP_278 \def (THead k t t0) in (let
-TMP_277 \def (THead k0 t t0) in (let TMP_279 \def (eq T TMP_278 TMP_277) in
-(let TMP_276 \def ((eq T (THead k t t0) (THead k0 t t0)) \to (\forall (P:
-Prop).P)) in (let TMP_280 \def (or TMP_279 TMP_276) in (let TMP_275 \def
-(\lambda (H10: (eq K k k0)).(let TMP_274 \def (\lambda (k1: K).(let TMP_272
-\def (THead k t t0) in (let TMP_271 \def (THead k1 t t0) in (let TMP_273 \def
-(eq T TMP_272 TMP_271) in (let TMP_270 \def ((eq T (THead k t t0) (THead k1 t
-t0)) \to (\forall (P: Prop).P)) in (or TMP_273 TMP_270)))))) in (let TMP_267
-\def (THead k t t0) in (let TMP_266 \def (THead k t t0) in (let TMP_268 \def
-(eq T TMP_267 TMP_266) in (let TMP_265 \def ((eq T (THead k t t0) (THead k t
-t0)) \to (\forall (P: Prop).P)) in (let TMP_263 \def (THead k t t0) in (let
-TMP_264 \def (refl_equal T TMP_263) in (let TMP_269 \def (or_introl TMP_268
-TMP_265 TMP_264) in (eq_ind K k TMP_274 TMP_269 k0 H10)))))))))) in (let
-TMP_262 \def (\lambda (H10: (((eq K k k0) \to (\forall (P: Prop).P)))).(let
-TMP_260 \def (THead k t t0) in (let TMP_259 \def (THead k0 t t0) in (let
-TMP_261 \def (eq T TMP_260 TMP_259) in (let TMP_258 \def ((eq T (THead k t
-t0) (THead k0 t t0)) \to (\forall (P: Prop).P)) in (let TMP_257 \def (\lambda
-(H11: (eq T (THead k t t0) (THead k0 t t0))).(\lambda (P: Prop).(let TMP_254
-\def (\lambda (e: T).(match e in T with [(TSort _) \Rightarrow k | (TLRef _)
-\Rightarrow k | (THead k1 _ _) \Rightarrow k1])) in (let TMP_253 \def (THead
-k t t0) in (let TMP_252 \def (THead k0 t t0) in (let H12 \def (f_equal T K
-TMP_254 TMP_253 TMP_252 H11) in (let TMP_255 \def (\lambda (k1: K).((eq K k
-k1) \to (\forall (P0: Prop).P0))) in (let H13 \def (eq_ind_r K k0 TMP_255 H10
-k H12) in (let TMP_256 \def (refl_equal K k) in (H13 TMP_256 P)))))))))) in
-(or_intror TMP_261 TMP_258 TMP_257))))))) in (let TMP_283 \def (or_ind
-TMP_282 TMP_281 TMP_280 TMP_275 TMP_262 H9) in (eq_ind T t0 TMP_288 TMP_283
-t4 H7))))))))))))))))) in (let TMP_247 \def (\lambda (H7: (((eq T t0 t4) \to
-(\forall (P: Prop).P)))).(let TMP_245 \def (THead k t t0) in (let TMP_244
-\def (THead k0 t t4) in (let TMP_246 \def (eq T TMP_245 TMP_244) in (let
-TMP_243 \def ((eq T (THead k t t0) (THead k0 t t4)) \to (\forall (P:
-Prop).P)) in (let TMP_242 \def (\lambda (H8: (eq T (THead k t t0) (THead k0 t
-t4))).(\lambda (P: Prop).(let TMP_231 \def (\lambda (e: T).(match e in T with
-[(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k1 _ _)
-\Rightarrow k1])) in (let TMP_230 \def (THead k t t0) in (let TMP_229 \def
-(THead k0 t t4) in (let H9 \def (f_equal T K TMP_231 TMP_230 TMP_229 H8) in
-(let TMP_234 \def (\lambda (e: T).(match e in T with [(TSort _) \Rightarrow
-t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t5) \Rightarrow t5])) in (let
-TMP_233 \def (THead k t t0) in (let TMP_232 \def (THead k0 t t4) in (let H10
-\def (f_equal T T TMP_234 TMP_233 TMP_232 H8) in (let TMP_241 \def (\lambda
-(_: (eq K k k0)).(let TMP_235 \def (\lambda (t5: T).((eq T t0 t5) \to
-(\forall (P0: Prop).P0))) in (let H12 \def (eq_ind_r T t4 TMP_235 H7 t0 H10)
-in (let TMP_239 \def (\lambda (t5: T).(let TMP_237 \def (THead k t t0) in
-(let TMP_238 \def (eq T TMP_237 t5) in (let TMP_236 \def ((eq T (THead k t
-t0) t5) \to (\forall (P0: Prop).P0)) in (or TMP_238 TMP_236))))) in (let H13
-\def (eq_ind_r T t4 TMP_239 H2 t0 H10) in (let TMP_240 \def (refl_equal T t0)
-in (H12 TMP_240 P))))))) in (TMP_241 H9)))))))))))) in (or_intror TMP_246
-TMP_243 TMP_242))))))) in (let TMP_297 \def (or_ind TMP_296 TMP_295 TMP_294
-TMP_289 TMP_247 H6) in (eq_ind T t TMP_302 TMP_297 t3 H4))))))))))))))))) in
-(let TMP_224 \def (\lambda (H4: (((eq T t t3) \to (\forall (P:
-Prop).P)))).(let TMP_222 \def (THead k t t0) in (let TMP_221 \def (THead k0
-t3 t4) in (let TMP_223 \def (eq T TMP_222 TMP_221) in (let TMP_220 \def ((eq
-T (THead k t t0) (THead k0 t3 t4)) \to (\forall (P: Prop).P)) in (let TMP_219
-\def (\lambda (H5: (eq T (THead k t t0) (THead k0 t3 t4))).(\lambda (P:
-Prop).(let TMP_200 \def (\lambda (e: T).(match e in T with [(TSort _)
-\Rightarrow k | (TLRef _) \Rightarrow k | (THead k1 _ _) \Rightarrow k1])) in
-(let TMP_199 \def (THead k t t0) in (let TMP_198 \def (THead k0 t3 t4) in
-(let H6 \def (f_equal T K TMP_200 TMP_199 TMP_198 H5) in (let TMP_203 \def
-(\lambda (e: T).(match e in T with [(TSort _) \Rightarrow t | (TLRef _)
-\Rightarrow t | (THead _ t5 _) \Rightarrow t5])) in (let TMP_202 \def (THead
-k t t0) in (let TMP_201 \def (THead k0 t3 t4) in (let H7 \def (f_equal T T
-TMP_203 TMP_202 TMP_201 H5) in (let TMP_206 \def (\lambda (e: T).(match e in
-T with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ _ t5)
-\Rightarrow t5])) in (let TMP_205 \def (THead k t t0) in (let TMP_204 \def
-(THead k0 t3 t4) in (let H8 \def (f_equal T T TMP_206 TMP_205 TMP_204 H5) in
-(let TMP_217 \def (\lambda (H9: (eq T t t3)).(\lambda (_: (eq K k k0)).(let
-TMP_210 \def (\lambda (t5: T).(let TMP_208 \def (THead k t t0) in (let
-TMP_209 \def (eq T TMP_208 t5) in (let TMP_207 \def ((eq T (THead k t t0) t5)
-\to (\forall (P0: Prop).P0)) in (or TMP_209 TMP_207))))) in (let H11 \def
-(eq_ind_r T t4 TMP_210 H2 t0 H8) in (let TMP_211 \def (\lambda (t5: T).((eq T
-t t5) \to (\forall (P0: Prop).P0))) in (let H12 \def (eq_ind_r T t3 TMP_211
-H4 t H9) in (let TMP_215 \def (\lambda (t5: T).(let TMP_213 \def (THead k t
-t0) in (let TMP_214 \def (eq T TMP_213 t5) in (let TMP_212 \def ((eq T (THead
-k t t0) t5) \to (\forall (P0: Prop).P0)) in (or TMP_214 TMP_212))))) in (let
-H13 \def (eq_ind_r T t3 TMP_215 H1 t H9) in (let TMP_216 \def (refl_equal T
-t) in (H12 TMP_216 P)))))))))) in (let TMP_218 \def (TMP_217 H7) in (TMP_218
-H6))))))))))))))))) in (or_intror TMP_223 TMP_220 TMP_219))))))) in (or_ind
-TMP_310 TMP_309 TMP_308 TMP_303 TMP_224 H3))))))))))))))))) in (T_ind TMP_333
-TMP_329 TMP_320 TMP_311 t2))))))))))) in (T_ind TMP_447 TMP_444 TMP_389
-TMP_334 t1))))).
+Prop).P)))))).(\lambda (t2: T).(T_ind (\lambda (t3: T).(or (eq T (THead k t
+t0) t3) ((eq T (THead k t t0) t3) \to (\forall (P: Prop).P)))) (\lambda (n:
+nat).(or_intror (eq T (THead k t t0) (TSort n)) ((eq T (THead k t t0) (TSort
+n)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (THead k t t0) (TSort
+n))).(\lambda (P: Prop).(let H2 \def (eq_ind T (THead k t t0) (\lambda (ee:
+T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False
+| (THead _ _ _) \Rightarrow True])) I (TSort n) H1) in (False_ind P H2))))))
+(\lambda (n: nat).(or_intror (eq T (THead k t t0) (TLRef n)) ((eq T (THead k
+t t0) (TLRef n)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (THead k t
+t0) (TLRef n))).(\lambda (P: Prop).(let H2 \def (eq_ind T (THead k t t0)
+(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n) H1) in
+(False_ind P H2)))))) (\lambda (k0: K).(\lambda (t3: T).(\lambda (H1: (or (eq
+T (THead k t t0) t3) ((eq T (THead k t t0) t3) \to (\forall (P:
+Prop).P)))).(\lambda (t4: T).(\lambda (H2: (or (eq T (THead k t t0) t4) ((eq
+T (THead k t t0) t4) \to (\forall (P: Prop).P)))).(let H_x \def (H t3) in
+(let H3 \def H_x in (or_ind (eq T t t3) ((eq T t t3) \to (\forall (P:
+Prop).P)) (or (eq T (THead k t t0) (THead k0 t3 t4)) ((eq T (THead k t t0)
+(THead k0 t3 t4)) \to (\forall (P: Prop).P))) (\lambda (H4: (eq T t t3)).(let
+H5 \def (eq_ind_r T t3 (\lambda (t5: T).(or (eq T (THead k t t0) t5) ((eq T
+(THead k t t0) t5) \to (\forall (P: Prop).P)))) H1 t H4) in (eq_ind T t
+(\lambda (t5: T).(or (eq T (THead k t t0) (THead k0 t5 t4)) ((eq T (THead k t
+t0) (THead k0 t5 t4)) \to (\forall (P: Prop).P)))) (let H_x0 \def (H0 t4) in
+(let H6 \def H_x0 in (or_ind (eq T t0 t4) ((eq T t0 t4) \to (\forall (P:
+Prop).P)) (or (eq T (THead k t t0) (THead k0 t t4)) ((eq T (THead k t t0)
+(THead k0 t t4)) \to (\forall (P: Prop).P))) (\lambda (H7: (eq T t0 t4)).(let
+H8 \def (eq_ind_r T t4 (\lambda (t5: T).(or (eq T (THead k t t0) t5) ((eq T
+(THead k t t0) t5) \to (\forall (P: Prop).P)))) H2 t0 H7) in (eq_ind T t0
+(\lambda (t5: T).(or (eq T (THead k t t0) (THead k0 t t5)) ((eq T (THead k t
+t0) (THead k0 t t5)) \to (\forall (P: Prop).P)))) (let H_x1 \def
+(terms_props__kind_dec k k0) in (let H9 \def H_x1 in (or_ind (eq K k k0) ((eq
+K k k0) \to (\forall (P: Prop).P)) (or (eq T (THead k t t0) (THead k0 t t0))
+((eq T (THead k t t0) (THead k0 t t0)) \to (\forall (P: Prop).P))) (\lambda
+(H10: (eq K k k0)).(eq_ind K k (\lambda (k1: K).(or (eq T (THead k t t0)
+(THead k1 t t0)) ((eq T (THead k t t0) (THead k1 t t0)) \to (\forall (P:
+Prop).P)))) (or_introl (eq T (THead k t t0) (THead k t t0)) ((eq T (THead k t
+t0) (THead k t t0)) \to (\forall (P: Prop).P)) (refl_equal T (THead k t t0)))
+k0 H10)) (\lambda (H10: (((eq K k k0) \to (\forall (P: Prop).P)))).(or_intror
+(eq T (THead k t t0) (THead k0 t t0)) ((eq T (THead k t t0) (THead k0 t t0))
+\to (\forall (P: Prop).P)) (\lambda (H11: (eq T (THead k t t0) (THead k0 t
+t0))).(\lambda (P: Prop).(let H12 \def (f_equal T K (\lambda (e: T).(match e
+with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k1 _ _)
+\Rightarrow k1])) (THead k t t0) (THead k0 t t0) H11) in (let H13 \def
+(eq_ind_r K k0 (\lambda (k1: K).((eq K k k1) \to (\forall (P0: Prop).P0)))
+H10 k H12) in (H13 (refl_equal K k) P))))))) H9))) t4 H7))) (\lambda (H7:
+(((eq T t0 t4) \to (\forall (P: Prop).P)))).(or_intror (eq T (THead k t t0)
+(THead k0 t t4)) ((eq T (THead k t t0) (THead k0 t t4)) \to (\forall (P:
+Prop).P)) (\lambda (H8: (eq T (THead k t t0) (THead k0 t t4))).(\lambda (P:
+Prop).(let H9 \def (f_equal T K (\lambda (e: T).(match e with [(TSort _)
+\Rightarrow k | (TLRef _) \Rightarrow k | (THead k1 _ _) \Rightarrow k1]))
+(THead k t t0) (THead k0 t t4) H8) in ((let H10 \def (f_equal T T (\lambda
+(e: T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 |
+(THead _ _ t5) \Rightarrow t5])) (THead k t t0) (THead k0 t t4) H8) in
+(\lambda (_: (eq K k k0)).(let H12 \def (eq_ind_r T t4 (\lambda (t5: T).((eq
+T t0 t5) \to (\forall (P0: Prop).P0))) H7 t0 H10) in (let H13 \def (eq_ind_r
+T t4 (\lambda (t5: T).(or (eq T (THead k t t0) t5) ((eq T (THead k t t0) t5)
+\to (\forall (P0: Prop).P0)))) H2 t0 H10) in (H12 (refl_equal T t0) P)))))
+H9)))))) H6))) t3 H4))) (\lambda (H4: (((eq T t t3) \to (\forall (P:
+Prop).P)))).(or_intror (eq T (THead k t t0) (THead k0 t3 t4)) ((eq T (THead k
+t t0) (THead k0 t3 t4)) \to (\forall (P: Prop).P)) (\lambda (H5: (eq T (THead
+k t t0) (THead k0 t3 t4))).(\lambda (P: Prop).(let H6 \def (f_equal T K
+(\lambda (e: T).(match e with [(TSort _) \Rightarrow k | (TLRef _)
+\Rightarrow k | (THead k1 _ _) \Rightarrow k1])) (THead k t t0) (THead k0 t3
+t4) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with [(TSort
+_) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ t5 _) \Rightarrow t5]))
+(THead k t t0) (THead k0 t3 t4) H5) in ((let H8 \def (f_equal T T (\lambda
+(e: T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 |
+(THead _ _ t5) \Rightarrow t5])) (THead k t t0) (THead k0 t3 t4) H5) in
+(\lambda (H9: (eq T t t3)).(\lambda (_: (eq K k k0)).(let H11 \def (eq_ind_r
+T t4 (\lambda (t5: T).(or (eq T (THead k t t0) t5) ((eq T (THead k t t0) t5)
+\to (\forall (P0: Prop).P0)))) H2 t0 H8) in (let H12 \def (eq_ind_r T t3
+(\lambda (t5: T).((eq T t t5) \to (\forall (P0: Prop).P0))) H4 t H9) in (let
+H13 \def (eq_ind_r T t3 (\lambda (t5: T).(or (eq T (THead k t t0) t5) ((eq T
+(THead k t t0) t5) \to (\forall (P0: Prop).P0)))) H1 t H9) in (H12
+(refl_equal T t) P))))))) H7)) H6)))))) H3)))))))) t2))))))) t1).