- \lambda (t1: T).(T_ind (\lambda (t: T).(\forall (t2: T).(or (eq T t t2) ((eq
-T t t2) \to (\forall (P: Prop).P))))) (\lambda (n: nat).(\lambda (t2:
-T).(T_ind (\lambda (t: T).(or (eq T (TSort n) t) ((eq T (TSort n) t) \to
-(\forall (P: Prop).P)))) (\lambda (n0: nat).(let H_x \def (nat_dec n n0) in
-(let H \def H_x in (or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P:
-Prop).P)) (or (eq T (TSort n) (TSort n0)) ((eq T (TSort n) (TSort n0)) \to
-(\forall (P: Prop).P))) (\lambda (H0: (eq nat n n0)).(eq_ind nat n (\lambda
-(n1: nat).(or (eq T (TSort n) (TSort n1)) ((eq T (TSort n) (TSort n1)) \to
-(\forall (P: Prop).P)))) (or_introl (eq T (TSort n) (TSort n)) ((eq T (TSort
-n) (TSort n)) \to (\forall (P: Prop).P)) (refl_equal T (TSort n))) n0 H0))
-(\lambda (H0: (((eq nat n n0) \to (\forall (P: Prop).P)))).(or_intror (eq T
-(TSort n) (TSort n0)) ((eq T (TSort n) (TSort n0)) \to (\forall (P: Prop).P))
-(\lambda (H1: (eq T (TSort n) (TSort n0))).(\lambda (P: Prop).(let H2 \def
-(f_equal T nat (\lambda (e: T).(match e in T return (\lambda (_: T).nat) with
-[(TSort n1) \Rightarrow n1 | (TLRef _) \Rightarrow n | (THead _ _ _)
-\Rightarrow n])) (TSort n) (TSort n0) H1) in (let H3 \def (eq_ind_r nat n0
-(\lambda (n1: nat).((eq nat n n1) \to (\forall (P0: Prop).P0))) H0 n H2) in
-(H3 (refl_equal nat n) P))))))) H)))) (\lambda (n0: nat).(or_intror (eq T
-(TSort n) (TLRef n0)) ((eq T (TSort n) (TLRef n0)) \to (\forall (P: Prop).P))
-(\lambda (H: (eq T (TSort n) (TLRef n0))).(\lambda (P: Prop).(let H0 \def
-(eq_ind T (TSort n) (\lambda (ee: T).(match ee in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
-(THead _ _ _) \Rightarrow False])) I (TLRef n0) H) in (False_ind P H0))))))
-(\lambda (k: K).(\lambda (t: T).(\lambda (_: (or (eq T (TSort n) t) ((eq T
-(TSort n) t) \to (\forall (P: Prop).P)))).(\lambda (t0: T).(\lambda (_: (or
-(eq T (TSort n) t0) ((eq T (TSort n) t0) \to (\forall (P:
-Prop).P)))).(or_intror (eq T (TSort n) (THead k t t0)) ((eq T (TSort n)
-(THead k t t0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (TSort n)
-(THead k t t0))).(\lambda (P: Prop).(let H2 \def (eq_ind T (TSort n) (\lambda
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
-\Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow
-False])) I (THead k t t0) H1) in (False_ind P H2)))))))))) t2))) (\lambda (n:
-nat).(\lambda (t2: T).(T_ind (\lambda (t: T).(or (eq T (TLRef n) t) ((eq T
-(TLRef n) t) \to (\forall (P: Prop).P)))) (\lambda (n0: nat).(or_intror (eq T
-(TLRef n) (TSort n0)) ((eq T (TLRef n) (TSort n0)) \to (\forall (P: Prop).P))
-(\lambda (H: (eq T (TLRef n) (TSort n0))).(\lambda (P: Prop).(let H0 \def
-(eq_ind T (TLRef n) (\lambda (ee: T).(match ee in T return (\lambda (_:
-T).Prop) with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
-(THead _ _ _) \Rightarrow False])) I (TSort n0) H) in (False_ind P H0))))))
-(\lambda (n0: nat).(let H_x \def (nat_dec n n0) in (let H \def H_x in (or_ind
-(eq nat n n0) ((eq nat n n0) \to (\forall (P: Prop).P)) (or (eq T (TLRef n)
-(TLRef n0)) ((eq T (TLRef n) (TLRef n0)) \to (\forall (P: Prop).P))) (\lambda
-(H0: (eq nat n n0)).(eq_ind nat n (\lambda (n1: nat).(or (eq T (TLRef n)
-(TLRef n1)) ((eq T (TLRef n) (TLRef n1)) \to (\forall (P: Prop).P))))
-(or_introl (eq T (TLRef n) (TLRef n)) ((eq T (TLRef n) (TLRef n)) \to
-(\forall (P: Prop).P)) (refl_equal T (TLRef n))) n0 H0)) (\lambda (H0: (((eq
-nat n n0) \to (\forall (P: Prop).P)))).(or_intror (eq T (TLRef n) (TLRef n0))
-((eq T (TLRef n) (TLRef n0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T
-(TLRef n) (TLRef n0))).(\lambda (P: Prop).(let H2 \def (f_equal T nat
-(\lambda (e: T).(match e in T return (\lambda (_: T).nat) with [(TSort _)
-\Rightarrow n | (TLRef n1) \Rightarrow n1 | (THead _ _ _) \Rightarrow n]))
-(TLRef n) (TLRef n0) H1) in (let H3 \def (eq_ind_r nat n0 (\lambda (n1:
-nat).((eq nat n n1) \to (\forall (P0: Prop).P0))) H0 n H2) in (H3 (refl_equal
-nat n) P))))))) H)))) (\lambda (k: K).(\lambda (t: T).(\lambda (_: (or (eq T
-(TLRef n) t) ((eq T (TLRef n) t) \to (\forall (P: Prop).P)))).(\lambda (t0:
-T).(\lambda (_: (or (eq T (TLRef n) t0) ((eq T (TLRef n) t0) \to (\forall (P:
-Prop).P)))).(or_intror (eq T (TLRef n) (THead k t t0)) ((eq T (TLRef n)
-(THead k t t0)) \to (\forall (P: Prop).P)) (\lambda (H1: (eq T (TLRef n)
-(THead k t t0))).(\lambda (P: Prop).(let H2 \def (eq_ind T (TLRef n) (\lambda
-(ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
-\Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
-False])) I (THead k t t0) H1) in (False_ind P H2)))))))))) t2))) (\lambda (k:
-K).(\lambda (t: T).(\lambda (H: ((\forall (t2: T).(or (eq T t t2) ((eq T t
-t2) \to (\forall (P: Prop).P)))))).(\lambda (t0: T).(\lambda (H0: ((\forall
-(t2: T).(or (eq T t0 t2) ((eq T t0 t2) \to (\forall (P:
-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 in T return (\lambda (_: T).Prop) 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 in T
-return (\lambda (_: T).Prop) 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
-in T return (\lambda (_: T).K) 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
-in T return (\lambda (_: T).K) 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 in T return
-(\lambda (_: T).T) 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 in T return (\lambda (_: T).K) 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 in T return (\lambda (_: T).T) 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
-in T return (\lambda (_: T).T) 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).
-(* COMMENTS
-Initial nodes: 2821
-END *)
+ \lambda (t1: T).(let TMP_447 \def (\lambda (t: T).(\forall (t2: T).(let
+TMP_446 \def (eq T t t2) in (let TMP_445 \def ((eq T t t2) \to (\forall (P:
+Prop).P)) in (or TMP_446 TMP_445))))) in (let TMP_444 \def (\lambda (n:
+nat).(\lambda (t2: T).(let TMP_443 \def (\lambda (t: T).(let TMP_441 \def
+(TSort n) in (let TMP_442 \def (eq T TMP_441 t) in (let TMP_440 \def ((eq T
+(TSort n) t) \to (\forall (P: Prop).P)) in (or TMP_442 TMP_440))))) in (let
+TMP_439 \def (\lambda (n0: nat).(let H_x \def (nat_dec n n0) in (let H \def
+H_x in (let TMP_438 \def (eq nat n n0) in (let TMP_437 \def ((eq nat n n0)
+\to (\forall (P: Prop).P)) in (let TMP_434 \def (TSort n) in (let TMP_433
+\def (TSort n0) in (let TMP_435 \def (eq T TMP_434 TMP_433) in (let TMP_432
+\def ((eq T (TSort n) (TSort n0)) \to (\forall (P: Prop).P)) in (let TMP_436
+\def (or TMP_435 TMP_432) in (let TMP_431 \def (\lambda (H0: (eq nat n
+n0)).(let TMP_430 \def (\lambda (n1: nat).(let TMP_428 \def (TSort n) in (let
+TMP_427 \def (TSort n1) in (let TMP_429 \def (eq T TMP_428 TMP_427) in (let
+TMP_426 \def ((eq T (TSort n) (TSort n1)) \to (\forall (P: Prop).P)) in (or
+TMP_429 TMP_426)))))) in (let TMP_423 \def (TSort n) in (let TMP_422 \def
+(TSort n) in (let TMP_424 \def (eq T TMP_423 TMP_422) in (let TMP_421 \def
+((eq T (TSort n) (TSort n)) \to (\forall (P: Prop).P)) in (let TMP_419 \def
+(TSort n) in (let TMP_420 \def (refl_equal T TMP_419) in (let TMP_425 \def
+(or_introl TMP_424 TMP_421 TMP_420) in (eq_ind nat n TMP_430 TMP_425 n0
+H0)))))))))) in (let TMP_418 \def (\lambda (H0: (((eq nat n n0) \to (\forall
+(P: Prop).P)))).(let TMP_416 \def (TSort n) in (let TMP_415 \def (TSort n0)
+in (let TMP_417 \def (eq T TMP_416 TMP_415) in (let TMP_414 \def ((eq T
+(TSort n) (TSort n0)) \to (\forall (P: Prop).P)) in (let TMP_413 \def
+(\lambda (H1: (eq T (TSort n) (TSort n0))).(\lambda (P: Prop).(let TMP_410
+\def (\lambda (e: T).(match e in T with [(TSort n1) \Rightarrow n1 | (TLRef
+_) \Rightarrow n | (THead _ _ _) \Rightarrow n])) in (let TMP_409 \def (TSort
+n) in (let TMP_408 \def (TSort n0) in (let H2 \def (f_equal T nat TMP_410
+TMP_409 TMP_408 H1) in (let TMP_411 \def (\lambda (n1: nat).((eq nat n n1)
+\to (\forall (P0: Prop).P0))) in (let H3 \def (eq_ind_r nat n0 TMP_411 H0 n
+H2) in (let TMP_412 \def (refl_equal nat n) in (H3 TMP_412 P)))))))))) in
+(or_intror TMP_417 TMP_414 TMP_413))))))) in (or_ind TMP_438 TMP_437 TMP_436
+TMP_431 TMP_418 H))))))))))))) in (let TMP_407 \def (\lambda (n0: nat).(let
+TMP_405 \def (TSort n) in (let TMP_404 \def (TLRef n0) in (let TMP_406 \def
+(eq T TMP_405 TMP_404) in (let TMP_403 \def ((eq T (TSort n) (TLRef n0)) \to
+(\forall (P: Prop).P)) in (let TMP_402 \def (\lambda (H: (eq T (TSort n)
+(TLRef n0))).(\lambda (P: Prop).(let TMP_401 \def (TSort n) in (let TMP_400
+\def (\lambda (ee: T).(match ee in T with [(TSort _) \Rightarrow True |
+(TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) in (let
+TMP_399 \def (TLRef n0) in (let H0 \def (eq_ind T TMP_401 TMP_400 I TMP_399
+H) in (False_ind P H0))))))) in (or_intror TMP_406 TMP_403 TMP_402))))))) in
+(let TMP_398 \def (\lambda (k: K).(\lambda (t: T).(\lambda (_: (or (eq T
+(TSort n) t) ((eq T (TSort n) t) \to (\forall (P: Prop).P)))).(\lambda (t0:
+T).(\lambda (_: (or (eq T (TSort n) t0) ((eq T (TSort n) t0) \to (\forall (P:
+Prop).P)))).(let TMP_396 \def (TSort n) in (let TMP_395 \def (THead k t t0)
+in (let TMP_397 \def (eq T TMP_396 TMP_395) in (let TMP_394 \def ((eq T
+(TSort n) (THead k t t0)) \to (\forall (P: Prop).P)) in (let TMP_393 \def
+(\lambda (H1: (eq T (TSort n) (THead k t t0))).(\lambda (P: Prop).(let
+TMP_392 \def (TSort n) in (let TMP_391 \def (\lambda (ee: T).(match ee in T
+with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _
+_) \Rightarrow False])) in (let TMP_390 \def (THead k t t0) in (let H2 \def
+(eq_ind T TMP_392 TMP_391 I TMP_390 H1) in (False_ind P H2))))))) in
+(or_intror TMP_397 TMP_394 TMP_393))))))))))) in (T_ind TMP_443 TMP_439
+TMP_407 TMP_398 t2))))))) in (let TMP_389 \def (\lambda (n: nat).(\lambda
+(t2: T).(let TMP_388 \def (\lambda (t: T).(let TMP_386 \def (TLRef n) in (let
+TMP_387 \def (eq T TMP_386 t) in (let TMP_385 \def ((eq T (TLRef n) t) \to
+(\forall (P: Prop).P)) in (or TMP_387 TMP_385))))) in (let TMP_384 \def
+(\lambda (n0: nat).(let TMP_382 \def (TLRef n) in (let TMP_381 \def (TSort
+n0) in (let TMP_383 \def (eq T TMP_382 TMP_381) in (let TMP_380 \def ((eq T
+(TLRef n) (TSort n0)) \to (\forall (P: Prop).P)) in (let TMP_379 \def
+(\lambda (H: (eq T (TLRef n) (TSort n0))).(\lambda (P: Prop).(let TMP_378
+\def (TLRef n) in (let TMP_377 \def (\lambda (ee: T).(match ee in T with
+[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
+\Rightarrow False])) in (let TMP_376 \def (TSort n0) in (let H0 \def (eq_ind
+T TMP_378 TMP_377 I TMP_376 H) in (False_ind P H0))))))) in (or_intror
+TMP_383 TMP_380 TMP_379))))))) in (let TMP_375 \def (\lambda (n0: nat).(let
+H_x \def (nat_dec n n0) in (let H \def H_x in (let TMP_374 \def (eq nat n n0)
+in (let TMP_373 \def ((eq nat n n0) \to (\forall (P: Prop).P)) in (let
+TMP_370 \def (TLRef n) in (let TMP_369 \def (TLRef n0) in (let TMP_371 \def
+(eq T TMP_370 TMP_369) in (let TMP_368 \def ((eq T (TLRef n) (TLRef n0)) \to
+(\forall (P: Prop).P)) in (let TMP_372 \def (or TMP_371 TMP_368) in (let
+TMP_367 \def (\lambda (H0: (eq nat n n0)).(let TMP_366 \def (\lambda (n1:
+nat).(let TMP_364 \def (TLRef n) in (let TMP_363 \def (TLRef n1) in (let
+TMP_365 \def (eq T TMP_364 TMP_363) in (let TMP_362 \def ((eq T (TLRef n)
+(TLRef n1)) \to (\forall (P: Prop).P)) in (or TMP_365 TMP_362)))))) in (let
+TMP_359 \def (TLRef n) in (let TMP_358 \def (TLRef n) in (let TMP_360 \def
+(eq T TMP_359 TMP_358) in (let TMP_357 \def ((eq T (TLRef n) (TLRef n)) \to
+(\forall (P: Prop).P)) in (let TMP_355 \def (TLRef n) in (let TMP_356 \def
+(refl_equal T TMP_355) in (let TMP_361 \def (or_introl TMP_360 TMP_357
+TMP_356) in (eq_ind nat n TMP_366 TMP_361 n0 H0)))))))))) in (let TMP_354
+\def (\lambda (H0: (((eq nat n n0) \to (\forall (P: Prop).P)))).(let TMP_352
+\def (TLRef n) in (let TMP_351 \def (TLRef n0) in (let TMP_353 \def (eq T
+TMP_352 TMP_351) in (let TMP_350 \def ((eq T (TLRef n) (TLRef n0)) \to
+(\forall (P: Prop).P)) in (let TMP_349 \def (\lambda (H1: (eq T (TLRef n)
+(TLRef n0))).(\lambda (P: Prop).(let TMP_346 \def (\lambda (e: T).(match e in
+T with [(TSort _) \Rightarrow n | (TLRef n1) \Rightarrow n1 | (THead _ _ _)
+\Rightarrow n])) in (let TMP_345 \def (TLRef n) in (let TMP_344 \def (TLRef
+n0) in (let H2 \def (f_equal T nat TMP_346 TMP_345 TMP_344 H1) in (let
+TMP_347 \def (\lambda (n1: nat).((eq nat n n1) \to (\forall (P0: Prop).P0)))
+in (let H3 \def (eq_ind_r nat n0 TMP_347 H0 n H2) in (let TMP_348 \def
+(refl_equal nat n) in (H3 TMP_348 P)))))))))) in (or_intror TMP_353 TMP_350
+TMP_349))))))) in (or_ind TMP_374 TMP_373 TMP_372 TMP_367 TMP_354
+H))))))))))))) in (let TMP_343 \def (\lambda (k: K).(\lambda (t: T).(\lambda
+(_: (or (eq T (TLRef n) t) ((eq T (TLRef n) t) \to (\forall (P:
+Prop).P)))).(\lambda (t0: T).(\lambda (_: (or (eq T (TLRef n) t0) ((eq T
+(TLRef n) t0) \to (\forall (P: Prop).P)))).(let TMP_341 \def (TLRef n) in
+(let TMP_340 \def (THead k t t0) in (let TMP_342 \def (eq T TMP_341 TMP_340)
+in (let TMP_339 \def ((eq T (TLRef n) (THead k t t0)) \to (\forall (P:
+Prop).P)) in (let TMP_338 \def (\lambda (H1: (eq T (TLRef n) (THead k t
+t0))).(\lambda (P: Prop).(let TMP_337 \def (TLRef n) in (let TMP_336 \def
+(\lambda (ee: T).(match ee in T with [(TSort _) \Rightarrow False | (TLRef _)
+\Rightarrow True | (THead _ _ _) \Rightarrow False])) in (let TMP_335 \def
+(THead k t t0) in (let H2 \def (eq_ind T TMP_337 TMP_336 I TMP_335 H1) in
+(False_ind P H2))))))) in (or_intror TMP_342 TMP_339 TMP_338))))))))))) in
+(T_ind TMP_388 TMP_384 TMP_375 TMP_343 t2))))))) in (let TMP_334 \def
+(\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (t2: T).(or (eq T t
+t2) ((eq T t t2) \to (\forall (P: Prop).P)))))).(\lambda (t0: T).(\lambda
+(H0: ((\forall (t2: T).(or (eq T t0 t2) ((eq T t0 t2) \to (\forall (P:
+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))))).