- \lambda (t1: T).(let TMP_3 \def (\lambda (t: T).(\forall (t2: T).(let TMP_1
-\def (eq T t t2) in (let TMP_2 \def ((eq T t t2) \to (\forall (P: Prop).P))
-in (or TMP_1 TMP_2))))) in (let TMP_58 \def (\lambda (n: nat).(\lambda (t2:
-T).(let TMP_7 \def (\lambda (t: T).(let TMP_4 \def (TSort n) in (let TMP_5
-\def (eq T TMP_4 t) in (let TMP_6 \def ((eq T (TSort n) t) \to (\forall (P:
-Prop).P)) in (or TMP_5 TMP_6))))) in (let TMP_39 \def (\lambda (n0: nat).(let
-H_x \def (nat_dec n n0) in (let H \def H_x in (let TMP_8 \def (eq nat n n0)
-in (let TMP_9 \def ((eq nat n n0) \to (\forall (P: Prop).P)) in (let TMP_10
-\def (TSort n) in (let TMP_11 \def (TSort n0) in (let TMP_12 \def (eq T
-TMP_10 TMP_11) in (let TMP_13 \def ((eq T (TSort n) (TSort n0)) \to (\forall
-(P: Prop).P)) in (let TMP_14 \def (or TMP_12 TMP_13) in (let TMP_27 \def
-(\lambda (H0: (eq nat n n0)).(let TMP_19 \def (\lambda (n1: nat).(let TMP_15
-\def (TSort n) in (let TMP_16 \def (TSort n1) in (let TMP_17 \def (eq T
-TMP_15 TMP_16) in (let TMP_18 \def ((eq T (TSort n) (TSort n1)) \to (\forall
-(P: Prop).P)) in (or TMP_17 TMP_18)))))) in (let TMP_20 \def (TSort n) in
-(let TMP_21 \def (TSort n) in (let TMP_22 \def (eq T TMP_20 TMP_21) in (let
-TMP_23 \def ((eq T (TSort n) (TSort n)) \to (\forall (P: Prop).P)) in (let
-TMP_24 \def (TSort n) in (let TMP_25 \def (refl_equal T TMP_24) in (let
-TMP_26 \def (or_introl TMP_22 TMP_23 TMP_25) in (eq_ind nat n TMP_19 TMP_26
-n0 H0)))))))))) in (let TMP_38 \def (\lambda (H0: (((eq nat n n0) \to
-(\forall (P: Prop).P)))).(let TMP_28 \def (TSort n) in (let TMP_29 \def
-(TSort n0) in (let TMP_30 \def (eq T TMP_28 TMP_29) in (let TMP_31 \def ((eq
-T (TSort n) (TSort n0)) \to (\forall (P: Prop).P)) in (let TMP_37 \def
-(\lambda (H1: (eq T (TSort n) (TSort n0))).(\lambda (P: Prop).(let TMP_32
-\def (\lambda (e: T).(match e with [(TSort n1) \Rightarrow n1 | (TLRef _)
-\Rightarrow n | (THead _ _ _) \Rightarrow n])) in (let TMP_33 \def (TSort n)
-in (let TMP_34 \def (TSort n0) in (let H2 \def (f_equal T nat TMP_32 TMP_33
-TMP_34 H1) in (let TMP_35 \def (\lambda (n1: nat).((eq nat n n1) \to (\forall
-(P0: Prop).P0))) in (let H3 \def (eq_ind_r nat n0 TMP_35 H0 n H2) in (let
-TMP_36 \def (refl_equal nat n) in (H3 TMP_36 P)))))))))) in (or_intror TMP_30
-TMP_31 TMP_37))))))) in (or_ind TMP_8 TMP_9 TMP_14 TMP_27 TMP_38
-H))))))))))))) in (let TMP_48 \def (\lambda (n0: nat).(let TMP_40 \def (TSort
-n) in (let TMP_41 \def (TLRef n0) in (let TMP_42 \def (eq T TMP_40 TMP_41) in
-(let TMP_43 \def ((eq T (TSort n) (TLRef n0)) \to (\forall (P: Prop).P)) in
-(let TMP_47 \def (\lambda (H: (eq T (TSort n) (TLRef n0))).(\lambda (P:
-Prop).(let TMP_44 \def (TSort n) in (let TMP_45 \def (\lambda (ee: T).(match
-ee with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _
-_ _) \Rightarrow False])) in (let TMP_46 \def (TLRef n0) in (let H0 \def
-(eq_ind T TMP_44 TMP_45 I TMP_46 H) in (False_ind P H0))))))) in (or_intror
-TMP_42 TMP_43 TMP_47))))))) in (let TMP_57 \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_49 \def (TSort n) in (let
-TMP_50 \def (THead k t t0) in (let TMP_51 \def (eq T TMP_49 TMP_50) in (let
-TMP_52 \def ((eq T (TSort n) (THead k t t0)) \to (\forall (P: Prop).P)) in
-(let TMP_56 \def (\lambda (H1: (eq T (TSort n) (THead k t t0))).(\lambda (P:
-Prop).(let TMP_53 \def (TSort n) in (let TMP_54 \def (\lambda (ee: T).(match
-ee with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _
-_ _) \Rightarrow False])) in (let TMP_55 \def (THead k t t0) in (let H2 \def
-(eq_ind T TMP_53 TMP_54 I TMP_55 H1) in (False_ind P H2))))))) in (or_intror
-TMP_51 TMP_52 TMP_56))))))))))) in (T_ind TMP_7 TMP_39 TMP_48 TMP_57
-t2))))))) in (let TMP_113 \def (\lambda (n: nat).(\lambda (t2: T).(let TMP_62
-\def (\lambda (t: T).(let TMP_59 \def (TLRef n) in (let TMP_60 \def (eq T
-TMP_59 t) in (let TMP_61 \def ((eq T (TLRef n) t) \to (\forall (P: Prop).P))
-in (or TMP_60 TMP_61))))) in (let TMP_71 \def (\lambda (n0: nat).(let TMP_63
-\def (TLRef n) in (let TMP_64 \def (TSort n0) in (let TMP_65 \def (eq T
-TMP_63 TMP_64) in (let TMP_66 \def ((eq T (TLRef n) (TSort n0)) \to (\forall
-(P: Prop).P)) in (let TMP_70 \def (\lambda (H: (eq T (TLRef n) (TSort
-n0))).(\lambda (P: Prop).(let TMP_67 \def (TLRef n) in (let TMP_68 \def
-(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
-\Rightarrow True | (THead _ _ _) \Rightarrow False])) in (let TMP_69 \def
-(TSort n0) in (let H0 \def (eq_ind T TMP_67 TMP_68 I TMP_69 H) in (False_ind
-P H0))))))) in (or_intror TMP_65 TMP_66 TMP_70))))))) in (let TMP_103 \def
-(\lambda (n0: nat).(let H_x \def (nat_dec n n0) in (let H \def H_x in (let
-TMP_72 \def (eq nat n n0) in (let TMP_73 \def ((eq nat n n0) \to (\forall (P:
-Prop).P)) in (let TMP_74 \def (TLRef n) in (let TMP_75 \def (TLRef n0) in
-(let TMP_76 \def (eq T TMP_74 TMP_75) in (let TMP_77 \def ((eq T (TLRef n)
-(TLRef n0)) \to (\forall (P: Prop).P)) in (let TMP_78 \def (or TMP_76 TMP_77)
-in (let TMP_91 \def (\lambda (H0: (eq nat n n0)).(let TMP_83 \def (\lambda
-(n1: nat).(let TMP_79 \def (TLRef n) in (let TMP_80 \def (TLRef n1) in (let
-TMP_81 \def (eq T TMP_79 TMP_80) in (let TMP_82 \def ((eq T (TLRef n) (TLRef
-n1)) \to (\forall (P: Prop).P)) in (or TMP_81 TMP_82)))))) in (let TMP_84
-\def (TLRef n) in (let TMP_85 \def (TLRef n) in (let TMP_86 \def (eq T TMP_84
-TMP_85) in (let TMP_87 \def ((eq T (TLRef n) (TLRef n)) \to (\forall (P:
-Prop).P)) in (let TMP_88 \def (TLRef n) in (let TMP_89 \def (refl_equal T
-TMP_88) in (let TMP_90 \def (or_introl TMP_86 TMP_87 TMP_89) in (eq_ind nat n
-TMP_83 TMP_90 n0 H0)))))))))) in (let TMP_102 \def (\lambda (H0: (((eq nat n
-n0) \to (\forall (P: Prop).P)))).(let TMP_92 \def (TLRef n) in (let TMP_93
-\def (TLRef n0) in (let TMP_94 \def (eq T TMP_92 TMP_93) in (let TMP_95 \def
-((eq T (TLRef n) (TLRef n0)) \to (\forall (P: Prop).P)) in (let TMP_101 \def
-(\lambda (H1: (eq T (TLRef n) (TLRef n0))).(\lambda (P: Prop).(let TMP_96
-\def (\lambda (e: T).(match e with [(TSort _) \Rightarrow n | (TLRef n1)
-\Rightarrow n1 | (THead _ _ _) \Rightarrow n])) in (let TMP_97 \def (TLRef n)
-in (let TMP_98 \def (TLRef n0) in (let H2 \def (f_equal T nat TMP_96 TMP_97
-TMP_98 H1) in (let TMP_99 \def (\lambda (n1: nat).((eq nat n n1) \to (\forall
-(P0: Prop).P0))) in (let H3 \def (eq_ind_r nat n0 TMP_99 H0 n H2) in (let
-TMP_100 \def (refl_equal nat n) in (H3 TMP_100 P)))))))))) in (or_intror
-TMP_94 TMP_95 TMP_101))))))) in (or_ind TMP_72 TMP_73 TMP_78 TMP_91 TMP_102
-H))))))))))))) in (let TMP_112 \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_104 \def (TLRef n) in
-(let TMP_105 \def (THead k t t0) in (let TMP_106 \def (eq T TMP_104 TMP_105)
-in (let TMP_107 \def ((eq T (TLRef n) (THead k t t0)) \to (\forall (P:
-Prop).P)) in (let TMP_111 \def (\lambda (H1: (eq T (TLRef n) (THead k t
-t0))).(\lambda (P: Prop).(let TMP_108 \def (TLRef n) in (let TMP_109 \def
-(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
-\Rightarrow True | (THead _ _ _) \Rightarrow False])) in (let TMP_110 \def
-(THead k t t0) in (let H2 \def (eq_ind T TMP_108 TMP_109 I TMP_110 H1) in
-(False_ind P H2))))))) in (or_intror TMP_106 TMP_107 TMP_111))))))))))) in
-(T_ind TMP_62 TMP_71 TMP_103 TMP_112 t2))))))) in (let TMP_250 \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_117 \def (\lambda (t3: T).(let
-TMP_114 \def (THead k t t0) in (let TMP_115 \def (eq T TMP_114 t3) in (let
-TMP_116 \def ((eq T (THead k t t0) t3) \to (\forall (P: Prop).P)) in (or
-TMP_115 TMP_116))))) in (let TMP_126 \def (\lambda (n: nat).(let TMP_118 \def
-(THead k t t0) in (let TMP_119 \def (TSort n) in (let TMP_120 \def (eq T
-TMP_118 TMP_119) in (let TMP_121 \def ((eq T (THead k t t0) (TSort n)) \to
-(\forall (P: Prop).P)) in (let TMP_125 \def (\lambda (H1: (eq T (THead k t
-t0) (TSort n))).(\lambda (P: Prop).(let TMP_122 \def (THead k t t0) in (let
-TMP_123 \def (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
-(TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) in (let
-TMP_124 \def (TSort n) in (let H2 \def (eq_ind T TMP_122 TMP_123 I TMP_124
-H1) in (False_ind P H2))))))) in (or_intror TMP_120 TMP_121 TMP_125))))))) in
-(let TMP_135 \def (\lambda (n: nat).(let TMP_127 \def (THead k t t0) in (let
-TMP_128 \def (TLRef n) in (let TMP_129 \def (eq T TMP_127 TMP_128) in (let
-TMP_130 \def ((eq T (THead k t t0) (TLRef n)) \to (\forall (P: Prop).P)) in
-(let TMP_134 \def (\lambda (H1: (eq T (THead k t t0) (TLRef n))).(\lambda (P:
-Prop).(let TMP_131 \def (THead k t t0) in (let TMP_132 \def (\lambda (ee:
+ \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 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 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 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 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 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 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: