- \lambda (u: T).(let TMP_7 \def (\lambda (t: T).(\forall (i: nat).(\forall
-(h: nat).((le h i) \to (let TMP_1 \def (TLRef h) in (let TMP_2 \def (S h) in
-(let TMP_3 \def (S i) in (let TMP_4 \def (lift TMP_2 TMP_3 t) in (let TMP_5
-\def (S h) in (let TMP_6 \def (lift TMP_5 i t) in (subst1 i TMP_1 TMP_4
-TMP_6))))))))))) in (let TMP_34 \def (\lambda (n: nat).(\lambda (i:
-nat).(\lambda (h: nat).(\lambda (_: (le h i)).(let TMP_8 \def (TSort n) in
-(let TMP_13 \def (\lambda (t: T).(let TMP_9 \def (TLRef h) in (let TMP_10
-\def (S h) in (let TMP_11 \def (TSort n) in (let TMP_12 \def (lift TMP_10 i
-TMP_11) in (subst1 i TMP_9 t TMP_12)))))) in (let TMP_14 \def (TSort n) in
-(let TMP_17 \def (\lambda (t: T).(let TMP_15 \def (TLRef h) in (let TMP_16
-\def (TSort n) in (subst1 i TMP_15 TMP_16 t)))) in (let TMP_18 \def (TLRef h)
-in (let TMP_19 \def (TSort n) in (let TMP_20 \def (subst1_refl i TMP_18
-TMP_19) in (let TMP_21 \def (S h) in (let TMP_22 \def (TSort n) in (let
-TMP_23 \def (lift TMP_21 i TMP_22) in (let TMP_24 \def (S h) in (let TMP_25
-\def (lift_sort n TMP_24 i) in (let TMP_26 \def (eq_ind_r T TMP_14 TMP_17
-TMP_20 TMP_23 TMP_25) in (let TMP_27 \def (S h) in (let TMP_28 \def (S i) in
-(let TMP_29 \def (TSort n) in (let TMP_30 \def (lift TMP_27 TMP_28 TMP_29) in
-(let TMP_31 \def (S h) in (let TMP_32 \def (S i) in (let TMP_33 \def
-(lift_sort n TMP_31 TMP_32) in (eq_ind_r T TMP_8 TMP_13 TMP_26 TMP_30
-TMP_33))))))))))))))))))))))))) in (let TMP_220 \def (\lambda (n:
-nat).(\lambda (i: nat).(\lambda (h: nat).(\lambda (H: (le h i)).(let TMP_35
-\def (TLRef h) in (let TMP_36 \def (S h) in (let TMP_37 \def (S i) in (let
-TMP_38 \def (TLRef n) in (let TMP_39 \def (lift TMP_36 TMP_37 TMP_38) in (let
-TMP_40 \def (S h) in (let TMP_41 \def (TLRef n) in (let TMP_42 \def (lift
-TMP_40 i TMP_41) in (let TMP_43 \def (subst1 i TMP_35 TMP_39 TMP_42) in (let
-TMP_79 \def (\lambda (H0: (lt n i)).(let TMP_44 \def (TLRef n) in (let TMP_49
-\def (\lambda (t: T).(let TMP_45 \def (TLRef h) in (let TMP_46 \def (S h) in
-(let TMP_47 \def (TLRef n) in (let TMP_48 \def (lift TMP_46 i TMP_47) in
-(subst1 i TMP_45 t TMP_48)))))) in (let TMP_50 \def (TLRef n) in (let TMP_53
-\def (\lambda (t: T).(let TMP_51 \def (TLRef h) in (let TMP_52 \def (TLRef n)
-in (subst1 i TMP_51 TMP_52 t)))) in (let TMP_54 \def (TLRef h) in (let TMP_55
-\def (TLRef n) in (let TMP_56 \def (subst1_refl i TMP_54 TMP_55) in (let
-TMP_57 \def (S h) in (let TMP_58 \def (TLRef n) in (let TMP_59 \def (lift
-TMP_57 i TMP_58) in (let TMP_60 \def (S h) in (let TMP_61 \def (lift_lref_lt
-n TMP_60 i H0) in (let TMP_62 \def (eq_ind_r T TMP_50 TMP_53 TMP_56 TMP_59
-TMP_61) in (let TMP_63 \def (S h) in (let TMP_64 \def (S i) in (let TMP_65
-\def (TLRef n) in (let TMP_66 \def (lift TMP_63 TMP_64 TMP_65) in (let TMP_67
-\def (S h) in (let TMP_68 \def (S i) in (let TMP_69 \def (S n) in (let TMP_70
-\def (S i) in (let TMP_71 \def (S n) in (let TMP_72 \def (S TMP_71) in (let
-TMP_73 \def (S i) in (let TMP_74 \def (S n) in (let TMP_75 \def (le_n_S
-TMP_74 i H0) in (let TMP_76 \def (le_S TMP_72 TMP_73 TMP_75) in (let TMP_77
-\def (le_S_n TMP_69 TMP_70 TMP_76) in (let TMP_78 \def (lift_lref_lt n TMP_67
-TMP_68 TMP_77) in (eq_ind_r T TMP_44 TMP_49 TMP_62 TMP_66
-TMP_78))))))))))))))))))))))))))))))) in (let TMP_174 \def (\lambda (H0: (eq
-nat n i)).(let TMP_80 \def (\lambda (n0: nat).(le h n0)) in (let H1 \def
-(eq_ind_r nat i TMP_80 H n H0) in (let TMP_89 \def (\lambda (n0: nat).(let
-TMP_81 \def (TLRef h) in (let TMP_82 \def (S h) in (let TMP_83 \def (S n0) in
-(let TMP_84 \def (TLRef n) in (let TMP_85 \def (lift TMP_82 TMP_83 TMP_84) in
-(let TMP_86 \def (S h) in (let TMP_87 \def (TLRef n) in (let TMP_88 \def
-(lift TMP_86 n0 TMP_87) in (subst1 n0 TMP_81 TMP_85 TMP_88)))))))))) in (let
-TMP_90 \def (TLRef n) in (let TMP_95 \def (\lambda (t: T).(let TMP_91 \def
-(TLRef h) in (let TMP_92 \def (S h) in (let TMP_93 \def (TLRef n) in (let
-TMP_94 \def (lift TMP_92 n TMP_93) in (subst1 n TMP_91 t TMP_94)))))) in (let
-TMP_96 \def (S h) in (let TMP_97 \def (plus n TMP_96) in (let TMP_98 \def
-(TLRef TMP_97) in (let TMP_101 \def (\lambda (t: T).(let TMP_99 \def (TLRef
-h) in (let TMP_100 \def (TLRef n) in (subst1 n TMP_99 TMP_100 t)))) in (let
-TMP_102 \def (plus n h) in (let TMP_103 \def (S TMP_102) in (let TMP_107 \def
-(\lambda (n0: nat).(let TMP_104 \def (TLRef h) in (let TMP_105 \def (TLRef n)
-in (let TMP_106 \def (TLRef n0) in (subst1 n TMP_104 TMP_105 TMP_106))))) in
-(let TMP_108 \def (plus h n) in (let TMP_113 \def (\lambda (n0: nat).(let
-TMP_109 \def (TLRef h) in (let TMP_110 \def (TLRef n) in (let TMP_111 \def (S
-n0) in (let TMP_112 \def (TLRef TMP_111) in (subst1 n TMP_109 TMP_110
-TMP_112)))))) in (let TMP_114 \def (S n) in (let TMP_115 \def (plus h
-TMP_114) in (let TMP_119 \def (\lambda (n0: nat).(let TMP_116 \def (TLRef h)
-in (let TMP_117 \def (TLRef n) in (let TMP_118 \def (TLRef n0) in (subst1 n
-TMP_116 TMP_117 TMP_118))))) in (let TMP_120 \def (S n) in (let TMP_121 \def
-(TLRef h) in (let TMP_122 \def (lift TMP_120 O TMP_121) in (let TMP_125 \def
-(\lambda (t: T).(let TMP_123 \def (TLRef h) in (let TMP_124 \def (TLRef n) in
-(subst1 n TMP_123 TMP_124 t)))) in (let TMP_126 \def (TLRef h) in (let
-TMP_127 \def (TLRef n) in (let TMP_128 \def (S n) in (let TMP_129 \def (TLRef
-h) in (let TMP_130 \def (lift TMP_128 O TMP_129) in (let TMP_131 \def (TLRef
-h) in (let TMP_132 \def (subst0_lref TMP_131 n) in (let TMP_133 \def
-(subst1_single n TMP_126 TMP_127 TMP_130 TMP_132) in (let TMP_134 \def (S n)
-in (let TMP_135 \def (plus h TMP_134) in (let TMP_136 \def (TLRef TMP_135) in
-(let TMP_137 \def (S n) in (let TMP_138 \def (le_O_n h) in (let TMP_139 \def
-(lift_lref_ge h TMP_137 O TMP_138) in (let TMP_140 \def (eq_ind T TMP_122
-TMP_125 TMP_133 TMP_136 TMP_139) in (let TMP_141 \def (plus h n) in (let
-TMP_142 \def (S TMP_141) in (let TMP_143 \def (plus h n) in (let TMP_144 \def
-(S TMP_143) in (let TMP_145 \def (S n) in (let TMP_146 \def (plus h TMP_145)
-in (let TMP_147 \def (plus_n_Sm h n) in (let TMP_148 \def (sym_eq nat TMP_144
-TMP_146 TMP_147) in (let TMP_149 \def (eq_ind nat TMP_115 TMP_119 TMP_140
-TMP_142 TMP_148) in (let TMP_150 \def (plus n h) in (let TMP_151 \def
-(plus_sym n h) in (let TMP_152 \def (eq_ind_r nat TMP_108 TMP_113 TMP_149
-TMP_150 TMP_151) in (let TMP_153 \def (S h) in (let TMP_154 \def (plus n
-TMP_153) in (let TMP_155 \def (plus_n_Sm n h) in (let TMP_156 \def (eq_ind
-nat TMP_103 TMP_107 TMP_152 TMP_154 TMP_155) in (let TMP_157 \def (S h) in
-(let TMP_158 \def (TLRef n) in (let TMP_159 \def (lift TMP_157 n TMP_158) in
-(let TMP_160 \def (S h) in (let TMP_161 \def (le_n n) in (let TMP_162 \def
-(lift_lref_ge n TMP_160 n TMP_161) in (let TMP_163 \def (eq_ind_r T TMP_98
-TMP_101 TMP_156 TMP_159 TMP_162) in (let TMP_164 \def (S h) in (let TMP_165
-\def (S n) in (let TMP_166 \def (TLRef n) in (let TMP_167 \def (lift TMP_164
-TMP_165 TMP_166) in (let TMP_168 \def (S h) in (let TMP_169 \def (S n) in
-(let TMP_170 \def (S n) in (let TMP_171 \def (le_n TMP_170) in (let TMP_172
-\def (lift_lref_lt n TMP_168 TMP_169 TMP_171) in (let TMP_173 \def (eq_ind_r
-T TMP_90 TMP_95 TMP_163 TMP_167 TMP_172) in (eq_ind nat n TMP_89 TMP_173 i
-H0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
-(let TMP_219 \def (\lambda (H0: (lt i n)).(let TMP_175 \def (S h) in (let
-TMP_176 \def (plus n TMP_175) in (let TMP_177 \def (TLRef TMP_176) in (let
-TMP_182 \def (\lambda (t: T).(let TMP_178 \def (TLRef h) in (let TMP_179 \def
-(S h) in (let TMP_180 \def (TLRef n) in (let TMP_181 \def (lift TMP_179 i
-TMP_180) in (subst1 i TMP_178 t TMP_181)))))) in (let TMP_183 \def (S h) in
-(let TMP_184 \def (plus n TMP_183) in (let TMP_185 \def (TLRef TMP_184) in
-(let TMP_190 \def (\lambda (t: T).(let TMP_186 \def (TLRef h) in (let TMP_187
-\def (S h) in (let TMP_188 \def (plus n TMP_187) in (let TMP_189 \def (TLRef
-TMP_188) in (subst1 i TMP_186 TMP_189 t)))))) in (let TMP_191 \def (TLRef h)
-in (let TMP_192 \def (S h) in (let TMP_193 \def (plus n TMP_192) in (let
-TMP_194 \def (TLRef TMP_193) in (let TMP_195 \def (subst1_refl i TMP_191
-TMP_194) in (let TMP_196 \def (S h) in (let TMP_197 \def (TLRef n) in (let
-TMP_198 \def (lift TMP_196 i TMP_197) in (let TMP_199 \def (S h) in (let
-TMP_200 \def (S i) in (let TMP_201 \def (S n) in (let TMP_202 \def (S i) in
-(let TMP_203 \def (S TMP_202) in (let TMP_204 \def (S n) in (let TMP_205 \def
-(S i) in (let TMP_206 \def (le_n_S TMP_205 n H0) in (let TMP_207 \def (le_S
-TMP_203 TMP_204 TMP_206) in (let TMP_208 \def (le_S_n TMP_200 TMP_201
-TMP_207) in (let TMP_209 \def (le_S_n i n TMP_208) in (let TMP_210 \def
-(lift_lref_ge n TMP_199 i TMP_209) in (let TMP_211 \def (eq_ind_r T TMP_185
-TMP_190 TMP_195 TMP_198 TMP_210) in (let TMP_212 \def (S h) in (let TMP_213
-\def (S i) in (let TMP_214 \def (TLRef n) in (let TMP_215 \def (lift TMP_212
-TMP_213 TMP_214) in (let TMP_216 \def (S h) in (let TMP_217 \def (S i) in
-(let TMP_218 \def (lift_lref_ge n TMP_216 TMP_217 H0) in (eq_ind_r T TMP_177
-TMP_182 TMP_211 TMP_215 TMP_218)))))))))))))))))))))))))))))))))))))) in
-(lt_eq_gt_e n i TMP_43 TMP_79 TMP_174 TMP_219))))))))))))))))) in (let
-TMP_297 \def (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (i:
+ \lambda (u: T).(T_ind (\lambda (t: T).(\forall (i: nat).(\forall (h:
+nat).((le h i) \to (subst1 i (TLRef h) (lift (S h) (S i) t) (lift (S h) i
+t)))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (h: nat).(\lambda (_:
+(le h i)).(eq_ind_r T (TSort n) (\lambda (t: T).(subst1 i (TLRef h) t (lift
+(S h) i (TSort n)))) (eq_ind_r T (TSort n) (\lambda (t: T).(subst1 i (TLRef
+h) (TSort n) t)) (subst1_refl i (TLRef h) (TSort n)) (lift (S h) i (TSort n))
+(lift_sort n (S h) i)) (lift (S h) (S i) (TSort n)) (lift_sort n (S h) (S
+i))))))) (\lambda (n: nat).(\lambda (i: nat).(\lambda (h: nat).(\lambda (H:
+(le h i)).(lt_eq_gt_e n i (subst1 i (TLRef h) (lift (S h) (S i) (TLRef n))
+(lift (S h) i (TLRef n))) (\lambda (H0: (lt n i)).(eq_ind_r T (TLRef n)
+(\lambda (t: T).(subst1 i (TLRef h) t (lift (S h) i (TLRef n)))) (eq_ind_r T
+(TLRef n) (\lambda (t: T).(subst1 i (TLRef h) (TLRef n) t)) (subst1_refl i
+(TLRef h) (TLRef n)) (lift (S h) i (TLRef n)) (lift_lref_lt n (S h) i H0))
+(lift (S h) (S i) (TLRef n)) (lift_lref_lt n (S h) (S i) (le_S_n (S n) (S i)
+(le_S (S (S n)) (S i) (le_n_S (S n) i H0)))))) (\lambda (H0: (eq nat n
+i)).(let H1 \def (eq_ind_r nat i (\lambda (n0: nat).(le h n0)) H n H0) in
+(eq_ind nat n (\lambda (n0: nat).(subst1 n0 (TLRef h) (lift (S h) (S n0)
+(TLRef n)) (lift (S h) n0 (TLRef n)))) (eq_ind_r T (TLRef n) (\lambda (t:
+T).(subst1 n (TLRef h) t (lift (S h) n (TLRef n)))) (eq_ind_r T (TLRef (plus
+n (S h))) (\lambda (t: T).(subst1 n (TLRef h) (TLRef n) t)) (eq_ind nat (S
+(plus n h)) (\lambda (n0: nat).(subst1 n (TLRef h) (TLRef n) (TLRef n0)))
+(eq_ind_r nat (plus h n) (\lambda (n0: nat).(subst1 n (TLRef h) (TLRef n)
+(TLRef (S n0)))) (eq_ind nat (plus h (S n)) (\lambda (n0: nat).(subst1 n
+(TLRef h) (TLRef n) (TLRef n0))) (eq_ind T (lift (S n) O (TLRef h)) (\lambda
+(t: T).(subst1 n (TLRef h) (TLRef n) t)) (subst1_single n (TLRef h) (TLRef n)
+(lift (S n) O (TLRef h)) (subst0_lref (TLRef h) n)) (TLRef (plus h (S n)))
+(lift_lref_ge h (S n) O (le_O_n h))) (S (plus h n)) (sym_eq nat (S (plus h
+n)) (plus h (S n)) (plus_n_Sm h n))) (plus n h) (plus_sym n h)) (plus n (S
+h)) (plus_n_Sm n h)) (lift (S h) n (TLRef n)) (lift_lref_ge n (S h) n (le_n
+n))) (lift (S h) (S n) (TLRef n)) (lift_lref_lt n (S h) (S n) (le_n (S n))))
+i H0))) (\lambda (H0: (lt i n)).(eq_ind_r T (TLRef (plus n (S h))) (\lambda
+(t: T).(subst1 i (TLRef h) t (lift (S h) i (TLRef n)))) (eq_ind_r T (TLRef
+(plus n (S h))) (\lambda (t: T).(subst1 i (TLRef h) (TLRef (plus n (S h)))
+t)) (subst1_refl i (TLRef h) (TLRef (plus n (S h)))) (lift (S h) i (TLRef n))
+(lift_lref_ge n (S h) i (le_S_n i n (le_S_n (S i) (S n) (le_S (S (S i)) (S n)
+(le_n_S (S i) n H0)))))) (lift (S h) (S i) (TLRef n)) (lift_lref_ge n (S h)
+(S i) H0)))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (i: