-h d c0 c)).(let TMP_12 \def (TSort m) in (let TMP_16 \def (\lambda (t:
-T).(let TMP_13 \def (next g m) in (let TMP_14 \def (TSort TMP_13) in (let
-TMP_15 \def (lift h d TMP_14) in (ty3 g c0 t TMP_15))))) in (let TMP_17 \def
-(next g m) in (let TMP_18 \def (TSort TMP_17) in (let TMP_20 \def (\lambda
-(t: T).(let TMP_19 \def (TSort m) in (ty3 g c0 TMP_19 t))) in (let TMP_21
-\def (ty3_sort g c0 m) in (let TMP_22 \def (next g m) in (let TMP_23 \def
-(TSort TMP_22) in (let TMP_24 \def (lift h d TMP_23) in (let TMP_25 \def
-(next g m) in (let TMP_26 \def (lift_sort TMP_25 h d) in (let TMP_27 \def
-(eq_ind_r T TMP_18 TMP_20 TMP_21 TMP_24 TMP_26) in (let TMP_28 \def (TSort m)
-in (let TMP_29 \def (lift h d TMP_28) in (let TMP_30 \def (lift_sort m h d)
-in (eq_ind_r T TMP_12 TMP_16 TMP_27 TMP_29 TMP_30)))))))))))))))))))))) in
-(let TMP_233 \def (\lambda (n: nat).(\lambda (c: C).(\lambda (d: C).(\lambda
-(u: T).(\lambda (H0: (getl n c (CHead d (Bind Abbr) u))).(\lambda (t:
-T).(\lambda (H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c0: C).(\forall (d0:
-nat).(\forall (h: nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u) (lift h
-d0 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h: nat).(\lambda
-(H3: (drop h d0 c0 c)).(let TMP_32 \def (TLRef n) in (let TMP_33 \def (lift h
-d0 TMP_32) in (let TMP_34 \def (S n) in (let TMP_35 \def (lift TMP_34 O t) in
-(let TMP_36 \def (lift h d0 TMP_35) in (let TMP_37 \def (ty3 g c0 TMP_33
-TMP_36) in (let TMP_159 \def (\lambda (H4: (lt n d0)).(let TMP_38 \def (S n)
-in (let TMP_39 \def (S d0) in (let TMP_40 \def (S n) in (let TMP_41 \def (S
-TMP_40) in (let TMP_42 \def (S d0) in (let TMP_43 \def (S n) in (let TMP_44
-\def (le_n_S TMP_43 d0 H4) in (let TMP_45 \def (le_S TMP_41 TMP_42 TMP_44) in
-(let TMP_46 \def (le_S_n TMP_38 TMP_39 TMP_45) in (let TMP_47 \def (le_S_n n
-d0 TMP_46) in (let TMP_48 \def (Bind Abbr) in (let TMP_49 \def (CHead d
-TMP_48 u) in (let H5 \def (drop_getl_trans_le n d0 TMP_47 c0 c h H3 TMP_49
-H0) in (let TMP_50 \def (\lambda (e0: C).(\lambda (_: C).(drop n O c0 e0)))
-in (let TMP_52 \def (\lambda (e0: C).(\lambda (e1: C).(let TMP_51 \def (minus
-d0 n) in (drop h TMP_51 e0 e1)))) in (let TMP_55 \def (\lambda (_:
-C).(\lambda (e1: C).(let TMP_53 \def (Bind Abbr) in (let TMP_54 \def (CHead d
-TMP_53 u) in (clear e1 TMP_54))))) in (let TMP_56 \def (TLRef n) in (let
-TMP_57 \def (lift h d0 TMP_56) in (let TMP_58 \def (S n) in (let TMP_59 \def
-(lift TMP_58 O t) in (let TMP_60 \def (lift h d0 TMP_59) in (let TMP_61 \def
-(ty3 g c0 TMP_57 TMP_60) in (let TMP_158 \def (\lambda (x0: C).(\lambda (x1:
-C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop h (minus d0 n) x0
-x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abbr) u))).(let TMP_62 \def
-(minus d0 n) in (let TMP_63 \def (\lambda (n0: nat).(drop h n0 x0 x1)) in
-(let TMP_64 \def (S n) in (let TMP_65 \def (minus d0 TMP_64) in (let TMP_66
-\def (S TMP_65) in (let TMP_67 \def (minus_x_Sy d0 n H4) in (let H9 \def
-(eq_ind nat TMP_62 TMP_63 H7 TMP_66 TMP_67) in (let TMP_68 \def (S n) in (let
-TMP_69 \def (minus d0 TMP_68) in (let H10 \def (drop_clear_S x1 x0 h TMP_69
-H9 Abbr d u H8) in (let TMP_75 \def (\lambda (c1: C).(let TMP_70 \def (Bind
-Abbr) in (let TMP_71 \def (S n) in (let TMP_72 \def (minus d0 TMP_71) in (let
-TMP_73 \def (lift h TMP_72 u) in (let TMP_74 \def (CHead c1 TMP_70 TMP_73) in
-(clear x0 TMP_74))))))) in (let TMP_78 \def (\lambda (c1: C).(let TMP_76 \def
-(S n) in (let TMP_77 \def (minus d0 TMP_76) in (drop h TMP_77 c1 d)))) in
-(let TMP_79 \def (TLRef n) in (let TMP_80 \def (lift h d0 TMP_79) in (let
-TMP_81 \def (S n) in (let TMP_82 \def (lift TMP_81 O t) in (let TMP_83 \def
-(lift h d0 TMP_82) in (let TMP_84 \def (ty3 g c0 TMP_80 TMP_83) in (let
-TMP_157 \def (\lambda (x: C).(\lambda (H11: (clear x0 (CHead x (Bind Abbr)
-(lift h (minus d0 (S n)) u)))).(\lambda (H12: (drop h (minus d0 (S n)) x
-d)).(let TMP_85 \def (TLRef n) in (let TMP_89 \def (\lambda (t0: T).(let
-TMP_86 \def (S n) in (let TMP_87 \def (lift TMP_86 O t) in (let TMP_88 \def
-(lift h d0 TMP_87) in (ty3 g c0 t0 TMP_88))))) in (let TMP_90 \def (S n) in
-(let TMP_91 \def (S n) in (let TMP_92 \def (minus d0 TMP_91) in (let TMP_93
-\def (plus TMP_90 TMP_92) in (let TMP_98 \def (\lambda (n0: nat).(let TMP_94
-\def (TLRef n) in (let TMP_95 \def (S n) in (let TMP_96 \def (lift TMP_95 O
-t) in (let TMP_97 \def (lift h n0 TMP_96) in (ty3 g c0 TMP_94 TMP_97)))))) in
-(let TMP_99 \def (S n) in (let TMP_100 \def (S n) in (let TMP_101 \def (minus
-d0 TMP_100) in (let TMP_102 \def (lift h TMP_101 t) in (let TMP_103 \def
-(lift TMP_99 O TMP_102) in (let TMP_105 \def (\lambda (t0: T).(let TMP_104
-\def (TLRef n) in (ty3 g c0 TMP_104 t0))) in (let TMP_112 \def (\lambda (_:
-nat).(let TMP_106 \def (TLRef n) in (let TMP_107 \def (S n) in (let TMP_108
-\def (S n) in (let TMP_109 \def (minus d0 TMP_108) in (let TMP_110 \def (lift
-h TMP_109 t) in (let TMP_111 \def (lift TMP_107 O TMP_110) in (ty3 g c0
-TMP_106 TMP_111)))))))) in (let TMP_113 \def (S n) in (let TMP_114 \def
-(minus d0 TMP_113) in (let TMP_115 \def (lift h TMP_114 u) in (let TMP_116
-\def (Bind Abbr) in (let TMP_117 \def (S n) in (let TMP_118 \def (minus d0
-TMP_117) in (let TMP_119 \def (lift h TMP_118 u) in (let TMP_120 \def (CHead
-x TMP_116 TMP_119) in (let TMP_121 \def (getl_intro n c0 TMP_120 x0 H6 H11)
-in (let TMP_122 \def (S n) in (let TMP_123 \def (minus d0 TMP_122) in (let
-TMP_124 \def (lift h TMP_123 t) in (let TMP_125 \def (S n) in (let TMP_126
-\def (minus d0 TMP_125) in (let TMP_127 \def (H2 x TMP_126 h H12) in (let
-TMP_128 \def (ty3_abbr g n c0 x TMP_115 TMP_121 TMP_124 TMP_127) in (let
-TMP_129 \def (S n) in (let TMP_130 \def (S n) in (let TMP_131 \def (minus d0
-TMP_130) in (let TMP_132 \def (plus TMP_129 TMP_131) in (let TMP_133 \def (S
-n) in (let TMP_134 \def (le_plus_minus TMP_133 d0 H4) in (let TMP_135 \def
-(eq_ind nat d0 TMP_112 TMP_128 TMP_132 TMP_134) in (let TMP_136 \def (S n) in
-(let TMP_137 \def (S n) in (let TMP_138 \def (minus d0 TMP_137) in (let
-TMP_139 \def (plus TMP_136 TMP_138) in (let TMP_140 \def (S n) in (let
-TMP_141 \def (lift TMP_140 O t) in (let TMP_142 \def (lift h TMP_139 TMP_141)
-in (let TMP_143 \def (S n) in (let TMP_144 \def (S n) in (let TMP_145 \def
-(minus d0 TMP_144) in (let TMP_146 \def (S n) in (let TMP_147 \def (minus d0
-TMP_146) in (let TMP_148 \def (le_O_n TMP_147) in (let TMP_149 \def (lift_d t
-h TMP_143 TMP_145 O TMP_148) in (let TMP_150 \def (eq_ind_r T TMP_103 TMP_105
-TMP_135 TMP_142 TMP_149) in (let TMP_151 \def (S n) in (let TMP_152 \def
-(le_plus_minus_r TMP_151 d0 H4) in (let TMP_153 \def (eq_ind nat TMP_93
-TMP_98 TMP_150 d0 TMP_152) in (let TMP_154 \def (TLRef n) in (let TMP_155
-\def (lift h d0 TMP_154) in (let TMP_156 \def (lift_lref_lt n h d0 H4) in
-(eq_ind_r T TMP_85 TMP_89 TMP_153 TMP_155
-TMP_156)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
-(ex2_ind C TMP_75 TMP_78 TMP_84 TMP_157 H10))))))))))))))))))))))))) in
-(ex3_2_ind C C TMP_50 TMP_52 TMP_55 TMP_61 TMP_158
-H5))))))))))))))))))))))))) in (let TMP_232 \def (\lambda (H4: (le d0
-n)).(let TMP_160 \def (plus n h) in (let TMP_161 \def (TLRef TMP_160) in (let
-TMP_165 \def (\lambda (t0: T).(let TMP_162 \def (S n) in (let TMP_163 \def
-(lift TMP_162 O t) in (let TMP_164 \def (lift h d0 TMP_163) in (ty3 g c0 t0
-TMP_164))))) in (let TMP_166 \def (S n) in (let TMP_172 \def (\lambda (_:
-nat).(let TMP_167 \def (plus n h) in (let TMP_168 \def (TLRef TMP_167) in
-(let TMP_169 \def (S n) in (let TMP_170 \def (lift TMP_169 O t) in (let
-TMP_171 \def (lift h d0 TMP_170) in (ty3 g c0 TMP_168 TMP_171))))))) in (let
-TMP_173 \def (S n) in (let TMP_174 \def (plus h TMP_173) in (let TMP_175 \def
-(lift TMP_174 O t) in (let TMP_178 \def (\lambda (t0: T).(let TMP_176 \def
-(plus n h) in (let TMP_177 \def (TLRef TMP_176) in (ty3 g c0 TMP_177 t0))))
-in (let TMP_179 \def (S n) in (let TMP_180 \def (plus TMP_179 h) in (let
-TMP_184 \def (\lambda (n0: nat).(let TMP_181 \def (plus n h) in (let TMP_182
-\def (TLRef TMP_181) in (let TMP_183 \def (lift n0 O t) in (ty3 g c0 TMP_182
-TMP_183))))) in (let TMP_185 \def (plus n h) in (let TMP_186 \def (Bind Abbr)
-in (let TMP_187 \def (CHead d TMP_186 u) in (let TMP_188 \def
-(drop_getl_trans_ge n c0 c d0 h H3 TMP_187 H0 H4) in (let TMP_189 \def
-(ty3_abbr g TMP_185 c0 d u TMP_188 t H1) in (let TMP_190 \def (S n) in (let
-TMP_191 \def (plus h TMP_190) in (let TMP_192 \def (S n) in (let TMP_193 \def
-(plus_sym h TMP_192) in (let TMP_194 \def (eq_ind_r nat TMP_180 TMP_184
-TMP_189 TMP_191 TMP_193) in (let TMP_195 \def (S n) in (let TMP_196 \def
-(lift TMP_195 O t) in (let TMP_197 \def (lift h d0 TMP_196) in (let TMP_198
-\def (S n) in (let TMP_199 \def (S n) in (let TMP_200 \def (S d0) in (let
-TMP_201 \def (S n) in (let TMP_202 \def (le_n_S d0 n H4) in (let TMP_203 \def
-(le_S TMP_200 TMP_201 TMP_202) in (let TMP_204 \def (le_S_n d0 TMP_199
-TMP_203) in (let TMP_205 \def (le_O_n d0) in (let TMP_206 \def (lift_free t
-TMP_198 h O d0 TMP_204 TMP_205) in (let TMP_207 \def (eq_ind_r T TMP_175
-TMP_178 TMP_194 TMP_197 TMP_206) in (let TMP_208 \def (S O) in (let TMP_209
-\def (plus n TMP_208) in (let TMP_210 \def (S O) in (let TMP_211 \def (plus
-TMP_210 n) in (let TMP_213 \def (\lambda (n0: nat).(let TMP_212 \def (S n) in
-(eq nat TMP_212 n0))) in (let TMP_214 \def (S n) in (let TMP_215 \def (S O)
-in (let TMP_216 \def (plus TMP_215 n) in (let TMP_217 \def (S O) in (let
-TMP_218 \def (plus TMP_217 n) in (let TMP_219 \def (le_n TMP_218) in (let
-TMP_220 \def (S n) in (let TMP_221 \def (le_n TMP_220) in (let TMP_222 \def
-(le_antisym TMP_214 TMP_216 TMP_219 TMP_221) in (let TMP_223 \def (S O) in
-(let TMP_224 \def (plus n TMP_223) in (let TMP_225 \def (S O) in (let TMP_226
-\def (plus_sym n TMP_225) in (let TMP_227 \def (eq_ind_r nat TMP_211 TMP_213
-TMP_222 TMP_224 TMP_226) in (let TMP_228 \def (eq_ind nat TMP_166 TMP_172
-TMP_207 TMP_209 TMP_227) in (let TMP_229 \def (TLRef n) in (let TMP_230 \def
-(lift h d0 TMP_229) in (let TMP_231 \def (lift_lref_ge n h d0 H4) in
-(eq_ind_r T TMP_161 TMP_165 TMP_228 TMP_230
-TMP_231)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
-(lt_le_e n d0 TMP_37 TMP_159 TMP_232))))))))))))))))))))) in (let TMP_435
-\def (\lambda (n: nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u:
-T).(\lambda (H0: (getl n c (CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda
-(H1: (ty3 g d u t)).(\lambda (H2: ((\forall (c0: C).(\forall (d0:
-nat).(\forall (h: nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u) (lift h
-d0 t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h: nat).(\lambda
-(H3: (drop h d0 c0 c)).(let TMP_234 \def (TLRef n) in (let TMP_235 \def (lift
-h d0 TMP_234) in (let TMP_236 \def (S n) in (let TMP_237 \def (lift TMP_236 O
-u) in (let TMP_238 \def (lift h d0 TMP_237) in (let TMP_239 \def (ty3 g c0
-TMP_235 TMP_238) in (let TMP_361 \def (\lambda (H4: (lt n d0)).(let TMP_240
-\def (S n) in (let TMP_241 \def (S d0) in (let TMP_242 \def (S n) in (let
-TMP_243 \def (S TMP_242) in (let TMP_244 \def (S d0) in (let TMP_245 \def (S
-n) in (let TMP_246 \def (le_n_S TMP_245 d0 H4) in (let TMP_247 \def (le_S
-TMP_243 TMP_244 TMP_246) in (let TMP_248 \def (le_S_n TMP_240 TMP_241
-TMP_247) in (let TMP_249 \def (le_S_n n d0 TMP_248) in (let TMP_250 \def
-(Bind Abst) in (let TMP_251 \def (CHead d TMP_250 u) in (let H5 \def
-(drop_getl_trans_le n d0 TMP_249 c0 c h H3 TMP_251 H0) in (let TMP_252 \def
-(\lambda (e0: C).(\lambda (_: C).(drop n O c0 e0))) in (let TMP_254 \def
-(\lambda (e0: C).(\lambda (e1: C).(let TMP_253 \def (minus d0 n) in (drop h
-TMP_253 e0 e1)))) in (let TMP_257 \def (\lambda (_: C).(\lambda (e1: C).(let
-TMP_255 \def (Bind Abst) in (let TMP_256 \def (CHead d TMP_255 u) in (clear
-e1 TMP_256))))) in (let TMP_258 \def (TLRef n) in (let TMP_259 \def (lift h
-d0 TMP_258) in (let TMP_260 \def (S n) in (let TMP_261 \def (lift TMP_260 O
-u) in (let TMP_262 \def (lift h d0 TMP_261) in (let TMP_263 \def (ty3 g c0
-TMP_259 TMP_262) in (let TMP_360 \def (\lambda (x0: C).(\lambda (x1:
-C).(\lambda (H6: (drop n O c0 x0)).(\lambda (H7: (drop h (minus d0 n) x0
-x1)).(\lambda (H8: (clear x1 (CHead d (Bind Abst) u))).(let TMP_264 \def
-(minus d0 n) in (let TMP_265 \def (\lambda (n0: nat).(drop h n0 x0 x1)) in
-(let TMP_266 \def (S n) in (let TMP_267 \def (minus d0 TMP_266) in (let
-TMP_268 \def (S TMP_267) in (let TMP_269 \def (minus_x_Sy d0 n H4) in (let H9
-\def (eq_ind nat TMP_264 TMP_265 H7 TMP_268 TMP_269) in (let TMP_270 \def (S
-n) in (let TMP_271 \def (minus d0 TMP_270) in (let H10 \def (drop_clear_S x1
-x0 h TMP_271 H9 Abst d u H8) in (let TMP_277 \def (\lambda (c1: C).(let
-TMP_272 \def (Bind Abst) in (let TMP_273 \def (S n) in (let TMP_274 \def
-(minus d0 TMP_273) in (let TMP_275 \def (lift h TMP_274 u) in (let TMP_276
-\def (CHead c1 TMP_272 TMP_275) in (clear x0 TMP_276))))))) in (let TMP_280
-\def (\lambda (c1: C).(let TMP_278 \def (S n) in (let TMP_279 \def (minus d0
-TMP_278) in (drop h TMP_279 c1 d)))) in (let TMP_281 \def (TLRef n) in (let
-TMP_282 \def (lift h d0 TMP_281) in (let TMP_283 \def (S n) in (let TMP_284
-\def (lift TMP_283 O u) in (let TMP_285 \def (lift h d0 TMP_284) in (let
-TMP_286 \def (ty3 g c0 TMP_282 TMP_285) in (let TMP_359 \def (\lambda (x:
-C).(\lambda (H11: (clear x0 (CHead x (Bind Abst) (lift h (minus d0 (S n))
-u)))).(\lambda (H12: (drop h (minus d0 (S n)) x d)).(let TMP_287 \def (TLRef
-n) in (let TMP_291 \def (\lambda (t0: T).(let TMP_288 \def (S n) in (let
-TMP_289 \def (lift TMP_288 O u) in (let TMP_290 \def (lift h d0 TMP_289) in
-(ty3 g c0 t0 TMP_290))))) in (let TMP_292 \def (S n) in (let TMP_293 \def (S
-n) in (let TMP_294 \def (minus d0 TMP_293) in (let TMP_295 \def (plus TMP_292
-TMP_294) in (let TMP_300 \def (\lambda (n0: nat).(let TMP_296 \def (TLRef n)
-in (let TMP_297 \def (S n) in (let TMP_298 \def (lift TMP_297 O u) in (let
-TMP_299 \def (lift h n0 TMP_298) in (ty3 g c0 TMP_296 TMP_299)))))) in (let
-TMP_301 \def (S n) in (let TMP_302 \def (S n) in (let TMP_303 \def (minus d0
-TMP_302) in (let TMP_304 \def (lift h TMP_303 u) in (let TMP_305 \def (lift
-TMP_301 O TMP_304) in (let TMP_307 \def (\lambda (t0: T).(let TMP_306 \def
-(TLRef n) in (ty3 g c0 TMP_306 t0))) in (let TMP_314 \def (\lambda (_:
-nat).(let TMP_308 \def (TLRef n) in (let TMP_309 \def (S n) in (let TMP_310
-\def (S n) in (let TMP_311 \def (minus d0 TMP_310) in (let TMP_312 \def (lift
-h TMP_311 u) in (let TMP_313 \def (lift TMP_309 O TMP_312) in (ty3 g c0
-TMP_308 TMP_313)))))))) in (let TMP_315 \def (S n) in (let TMP_316 \def
-(minus d0 TMP_315) in (let TMP_317 \def (lift h TMP_316 u) in (let TMP_318
-\def (Bind Abst) in (let TMP_319 \def (S n) in (let TMP_320 \def (minus d0
-TMP_319) in (let TMP_321 \def (lift h TMP_320 u) in (let TMP_322 \def (CHead
-x TMP_318 TMP_321) in (let TMP_323 \def (getl_intro n c0 TMP_322 x0 H6 H11)
-in (let TMP_324 \def (S n) in (let TMP_325 \def (minus d0 TMP_324) in (let
-TMP_326 \def (lift h TMP_325 t) in (let TMP_327 \def (S n) in (let TMP_328
-\def (minus d0 TMP_327) in (let TMP_329 \def (H2 x TMP_328 h H12) in (let
-TMP_330 \def (ty3_abst g n c0 x TMP_317 TMP_323 TMP_326 TMP_329) in (let
-TMP_331 \def (S n) in (let TMP_332 \def (S n) in (let TMP_333 \def (minus d0
-TMP_332) in (let TMP_334 \def (plus TMP_331 TMP_333) in (let TMP_335 \def (S
-n) in (let TMP_336 \def (le_plus_minus TMP_335 d0 H4) in (let TMP_337 \def
-(eq_ind nat d0 TMP_314 TMP_330 TMP_334 TMP_336) in (let TMP_338 \def (S n) in
-(let TMP_339 \def (S n) in (let TMP_340 \def (minus d0 TMP_339) in (let
-TMP_341 \def (plus TMP_338 TMP_340) in (let TMP_342 \def (S n) in (let
-TMP_343 \def (lift TMP_342 O u) in (let TMP_344 \def (lift h TMP_341 TMP_343)
-in (let TMP_345 \def (S n) in (let TMP_346 \def (S n) in (let TMP_347 \def
-(minus d0 TMP_346) in (let TMP_348 \def (S n) in (let TMP_349 \def (minus d0
-TMP_348) in (let TMP_350 \def (le_O_n TMP_349) in (let TMP_351 \def (lift_d u
-h TMP_345 TMP_347 O TMP_350) in (let TMP_352 \def (eq_ind_r T TMP_305 TMP_307
-TMP_337 TMP_344 TMP_351) in (let TMP_353 \def (S n) in (let TMP_354 \def
-(le_plus_minus_r TMP_353 d0 H4) in (let TMP_355 \def (eq_ind nat TMP_295
-TMP_300 TMP_352 d0 TMP_354) in (let TMP_356 \def (TLRef n) in (let TMP_357
-\def (lift h d0 TMP_356) in (let TMP_358 \def (lift_lref_lt n h d0 H4) in
-(eq_ind_r T TMP_287 TMP_291 TMP_355 TMP_357
-TMP_358)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
-(ex2_ind C TMP_277 TMP_280 TMP_286 TMP_359 H10))))))))))))))))))))))))) in
-(ex3_2_ind C C TMP_252 TMP_254 TMP_257 TMP_263 TMP_360
-H5))))))))))))))))))))))))) in (let TMP_434 \def (\lambda (H4: (le d0
-n)).(let TMP_362 \def (plus n h) in (let TMP_363 \def (TLRef TMP_362) in (let
-TMP_367 \def (\lambda (t0: T).(let TMP_364 \def (S n) in (let TMP_365 \def
-(lift TMP_364 O u) in (let TMP_366 \def (lift h d0 TMP_365) in (ty3 g c0 t0
-TMP_366))))) in (let TMP_368 \def (S n) in (let TMP_374 \def (\lambda (_:
-nat).(let TMP_369 \def (plus n h) in (let TMP_370 \def (TLRef TMP_369) in
-(let TMP_371 \def (S n) in (let TMP_372 \def (lift TMP_371 O u) in (let
-TMP_373 \def (lift h d0 TMP_372) in (ty3 g c0 TMP_370 TMP_373))))))) in (let
-TMP_375 \def (S n) in (let TMP_376 \def (plus h TMP_375) in (let TMP_377 \def
-(lift TMP_376 O u) in (let TMP_380 \def (\lambda (t0: T).(let TMP_378 \def
-(plus n h) in (let TMP_379 \def (TLRef TMP_378) in (ty3 g c0 TMP_379 t0))))
-in (let TMP_381 \def (S n) in (let TMP_382 \def (plus TMP_381 h) in (let
-TMP_386 \def (\lambda (n0: nat).(let TMP_383 \def (plus n h) in (let TMP_384
-\def (TLRef TMP_383) in (let TMP_385 \def (lift n0 O u) in (ty3 g c0 TMP_384
-TMP_385))))) in (let TMP_387 \def (plus n h) in (let TMP_388 \def (Bind Abst)
-in (let TMP_389 \def (CHead d TMP_388 u) in (let TMP_390 \def
-(drop_getl_trans_ge n c0 c d0 h H3 TMP_389 H0 H4) in (let TMP_391 \def
-(ty3_abst g TMP_387 c0 d u TMP_390 t H1) in (let TMP_392 \def (S n) in (let
-TMP_393 \def (plus h TMP_392) in (let TMP_394 \def (S n) in (let TMP_395 \def
-(plus_sym h TMP_394) in (let TMP_396 \def (eq_ind_r nat TMP_382 TMP_386
-TMP_391 TMP_393 TMP_395) in (let TMP_397 \def (S n) in (let TMP_398 \def
-(lift TMP_397 O u) in (let TMP_399 \def (lift h d0 TMP_398) in (let TMP_400
-\def (S n) in (let TMP_401 \def (S n) in (let TMP_402 \def (S d0) in (let
-TMP_403 \def (S n) in (let TMP_404 \def (le_n_S d0 n H4) in (let TMP_405 \def
-(le_S TMP_402 TMP_403 TMP_404) in (let TMP_406 \def (le_S_n d0 TMP_401
-TMP_405) in (let TMP_407 \def (le_O_n d0) in (let TMP_408 \def (lift_free u
-TMP_400 h O d0 TMP_406 TMP_407) in (let TMP_409 \def (eq_ind_r T TMP_377
-TMP_380 TMP_396 TMP_399 TMP_408) in (let TMP_410 \def (S O) in (let TMP_411
-\def (plus n TMP_410) in (let TMP_412 \def (S O) in (let TMP_413 \def (plus
-TMP_412 n) in (let TMP_415 \def (\lambda (n0: nat).(let TMP_414 \def (S n) in
-(eq nat TMP_414 n0))) in (let TMP_416 \def (S n) in (let TMP_417 \def (S O)
-in (let TMP_418 \def (plus TMP_417 n) in (let TMP_419 \def (S O) in (let
-TMP_420 \def (plus TMP_419 n) in (let TMP_421 \def (le_n TMP_420) in (let
-TMP_422 \def (S n) in (let TMP_423 \def (le_n TMP_422) in (let TMP_424 \def
-(le_antisym TMP_416 TMP_418 TMP_421 TMP_423) in (let TMP_425 \def (S O) in
-(let TMP_426 \def (plus n TMP_425) in (let TMP_427 \def (S O) in (let TMP_428
-\def (plus_sym n TMP_427) in (let TMP_429 \def (eq_ind_r nat TMP_413 TMP_415
-TMP_424 TMP_426 TMP_428) in (let TMP_430 \def (eq_ind nat TMP_368 TMP_374
-TMP_409 TMP_411 TMP_429) in (let TMP_431 \def (TLRef n) in (let TMP_432 \def
-(lift h d0 TMP_431) in (let TMP_433 \def (lift_lref_ge n h d0 H4) in
-(eq_ind_r T TMP_363 TMP_367 TMP_430 TMP_432
-TMP_433)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in
-(lt_le_e n d0 TMP_239 TMP_361 TMP_434))))))))))))))))))))) in (let TMP_484
-\def (\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c u
-t)).(\lambda (H1: ((\forall (c0: C).(\forall (d: nat).(\forall (h:
-nat).((drop h d c0 c) \to (ty3 g c0 (lift h d u) (lift h d t)))))))).(\lambda
-(b: B).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c (Bind
-b) u) t0 t3)).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall (h:
-nat).((drop h d c0 (CHead c (Bind b) u)) \to (ty3 g c0 (lift h d t0) (lift h
-d t3)))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda
-(H4: (drop h d c0 c)).(let TMP_436 \def (Bind b) in (let TMP_437 \def (lift h
-d u) in (let TMP_438 \def (Bind b) in (let TMP_439 \def (s TMP_438 d) in (let
-TMP_440 \def (lift h TMP_439 t0) in (let TMP_441 \def (THead TMP_436 TMP_437
-TMP_440) in (let TMP_445 \def (\lambda (t4: T).(let TMP_442 \def (Bind b) in
-(let TMP_443 \def (THead TMP_442 u t3) in (let TMP_444 \def (lift h d
-TMP_443) in (ty3 g c0 t4 TMP_444))))) in (let TMP_446 \def (Bind b) in (let
-TMP_447 \def (lift h d u) in (let TMP_448 \def (Bind b) in (let TMP_449 \def
-(s TMP_448 d) in (let TMP_450 \def (lift h TMP_449 t3) in (let TMP_451 \def
-(THead TMP_446 TMP_447 TMP_450) in (let TMP_458 \def (\lambda (t4: T).(let
-TMP_452 \def (Bind b) in (let TMP_453 \def (lift h d u) in (let TMP_454 \def
-(Bind b) in (let TMP_455 \def (s TMP_454 d) in (let TMP_456 \def (lift h
-TMP_455 t0) in (let TMP_457 \def (THead TMP_452 TMP_453 TMP_456) in (ty3 g c0
-TMP_457 t4)))))))) in (let TMP_459 \def (lift h d u) in (let TMP_460 \def
-(lift h d t) in (let TMP_461 \def (H1 c0 d h H4) in (let TMP_462 \def (S d)
-in (let TMP_463 \def (lift h TMP_462 t0) in (let TMP_464 \def (S d) in (let
-TMP_465 \def (lift h TMP_464 t3) in (let TMP_466 \def (Bind b) in (let
-TMP_467 \def (lift h d u) in (let TMP_468 \def (CHead c0 TMP_466 TMP_467) in
-(let TMP_469 \def (S d) in (let TMP_470 \def (drop_skip_bind h d c0 c H4 b u)
-in (let TMP_471 \def (H3 TMP_468 TMP_469 h TMP_470) in (let TMP_472 \def
-(ty3_bind g c0 TMP_459 TMP_460 TMP_461 b TMP_463 TMP_465 TMP_471) in (let
-TMP_473 \def (Bind b) in (let TMP_474 \def (THead TMP_473 u t3) in (let
-TMP_475 \def (lift h d TMP_474) in (let TMP_476 \def (Bind b) in (let TMP_477
-\def (lift_head TMP_476 u t3 h d) in (let TMP_478 \def (eq_ind_r T TMP_451
-TMP_458 TMP_472 TMP_475 TMP_477) in (let TMP_479 \def (Bind b) in (let
-TMP_480 \def (THead TMP_479 u t0) in (let TMP_481 \def (lift h d TMP_480) in
-(let TMP_482 \def (Bind b) in (let TMP_483 \def (lift_head TMP_482 u t0 h d)
-in (eq_ind_r T TMP_441 TMP_445 TMP_478 TMP_481
-TMP_483)))))))))))))))))))))))))))))))))))))))))))))))))))))) in (let TMP_577
-\def (\lambda (c: C).(\lambda (w: T).(\lambda (u: T).(\lambda (_: (ty3 g c w
-u)).(\lambda (H1: ((\forall (c0: C).(\forall (d: nat).(\forall (h:
-nat).((drop h d c0 c) \to (ty3 g c0 (lift h d w) (lift h d u)))))))).(\lambda
-(v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead (Bind Abst) u
-t))).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall (h:
-nat).((drop h d c0 c) \to (ty3 g c0 (lift h d v) (lift h d (THead (Bind Abst)
-u t))))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda
-(H4: (drop h d c0 c)).(let TMP_485 \def (Flat Appl) in (let TMP_486 \def
-(lift h d w) in (let TMP_487 \def (Flat Appl) in (let TMP_488 \def (s TMP_487
-d) in (let TMP_489 \def (lift h TMP_488 v) in (let TMP_490 \def (THead
-TMP_485 TMP_486 TMP_489) in (let TMP_496 \def (\lambda (t0: T).(let TMP_491
-\def (Flat Appl) in (let TMP_492 \def (Bind Abst) in (let TMP_493 \def (THead
-TMP_492 u t) in (let TMP_494 \def (THead TMP_491 w TMP_493) in (let TMP_495
-\def (lift h d TMP_494) in (ty3 g c0 t0 TMP_495))))))) in (let TMP_497 \def
-(Flat Appl) in (let TMP_498 \def (lift h d w) in (let TMP_499 \def (Flat
-Appl) in (let TMP_500 \def (s TMP_499 d) in (let TMP_501 \def (Bind Abst) in
-(let TMP_502 \def (THead TMP_501 u t) in (let TMP_503 \def (lift h TMP_500
-TMP_502) in (let TMP_504 \def (THead TMP_497 TMP_498 TMP_503) in (let TMP_511
-\def (\lambda (t0: T).(let TMP_505 \def (Flat Appl) in (let TMP_506 \def
-(lift h d w) in (let TMP_507 \def (Flat Appl) in (let TMP_508 \def (s TMP_507
-d) in (let TMP_509 \def (lift h TMP_508 v) in (let TMP_510 \def (THead
-TMP_505 TMP_506 TMP_509) in (ty3 g c0 TMP_510 t0)))))))) in (let TMP_512 \def
-(Bind Abst) in (let TMP_513 \def (Flat Appl) in (let TMP_514 \def (s TMP_513
-d) in (let TMP_515 \def (lift h TMP_514 u) in (let TMP_516 \def (Bind Abst)
-in (let TMP_517 \def (Flat Appl) in (let TMP_518 \def (s TMP_517 d) in (let
-TMP_519 \def (s TMP_516 TMP_518) in (let TMP_520 \def (lift h TMP_519 t) in
-(let TMP_521 \def (THead TMP_512 TMP_515 TMP_520) in (let TMP_531 \def
-(\lambda (t0: T).(let TMP_522 \def (Flat Appl) in (let TMP_523 \def (lift h d
-w) in (let TMP_524 \def (Flat Appl) in (let TMP_525 \def (s TMP_524 d) in
-(let TMP_526 \def (lift h TMP_525 v) in (let TMP_527 \def (THead TMP_522
-TMP_523 TMP_526) in (let TMP_528 \def (Flat Appl) in (let TMP_529 \def (lift
-h d w) in (let TMP_530 \def (THead TMP_528 TMP_529 t0) in (ty3 g c0 TMP_527
-TMP_530))))))))))) in (let TMP_532 \def (lift h d w) in (let TMP_533 \def
-(lift h d u) in (let TMP_534 \def (H1 c0 d h H4) in (let TMP_535 \def (lift h
-d v) in (let TMP_536 \def (S d) in (let TMP_537 \def (lift h TMP_536 t) in
-(let TMP_538 \def (Bind Abst) in (let TMP_539 \def (THead TMP_538 u t) in
-(let TMP_540 \def (lift h d TMP_539) in (let TMP_542 \def (\lambda (t0:
-T).(let TMP_541 \def (lift h d v) in (ty3 g c0 TMP_541 t0))) in (let TMP_543
-\def (H3 c0 d h H4) in (let TMP_544 \def (Bind Abst) in (let TMP_545 \def
-(lift h d u) in (let TMP_546 \def (S d) in (let TMP_547 \def (lift h TMP_546
-t) in (let TMP_548 \def (THead TMP_544 TMP_545 TMP_547) in (let TMP_549 \def
-(lift_bind Abst u t h d) in (let TMP_550 \def (eq_ind T TMP_540 TMP_542
-TMP_543 TMP_548 TMP_549) in (let TMP_551 \def (ty3_appl g c0 TMP_532 TMP_533
-TMP_534 TMP_535 TMP_537 TMP_550) in (let TMP_552 \def (Flat Appl) in (let
-TMP_553 \def (s TMP_552 d) in (let TMP_554 \def (Bind Abst) in (let TMP_555
-\def (THead TMP_554 u t) in (let TMP_556 \def (lift h TMP_553 TMP_555) in
-(let TMP_557 \def (Bind Abst) in (let TMP_558 \def (Flat Appl) in (let
-TMP_559 \def (s TMP_558 d) in (let TMP_560 \def (lift_head TMP_557 u t h
-TMP_559) in (let TMP_561 \def (eq_ind_r T TMP_521 TMP_531 TMP_551 TMP_556
-TMP_560) in (let TMP_562 \def (Flat Appl) in (let TMP_563 \def (Bind Abst) in
-(let TMP_564 \def (THead TMP_563 u t) in (let TMP_565 \def (THead TMP_562 w
-TMP_564) in (let TMP_566 \def (lift h d TMP_565) in (let TMP_567 \def (Flat
-Appl) in (let TMP_568 \def (Bind Abst) in (let TMP_569 \def (THead TMP_568 u
-t) in (let TMP_570 \def (lift_head TMP_567 w TMP_569 h d) in (let TMP_571
-\def (eq_ind_r T TMP_504 TMP_511 TMP_561 TMP_566 TMP_570) in (let TMP_572
-\def (Flat Appl) in (let TMP_573 \def (THead TMP_572 w v) in (let TMP_574
-\def (lift h d TMP_573) in (let TMP_575 \def (Flat Appl) in (let TMP_576 \def
-(lift_head TMP_575 w v h d) in (eq_ind_r T TMP_490 TMP_496 TMP_571 TMP_574
-TMP_576)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-)))))))))))))) in (let TMP_624 \def (\lambda (c: C).(\lambda (t0: T).(\lambda
-(t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda (H1: ((\forall (c0:
-C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h
-d t0) (lift h d t3)))))))).(\lambda (t4: T).(\lambda (_: (ty3 g c t3
-t4)).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall (h:
-nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t3) (lift h d
+h d c0 c)).(eq_ind_r T (TSort m) (\lambda (t: T).(ty3 g c0 t (lift h d (TSort
+(next g m))))) (eq_ind_r T (TSort (next g m)) (\lambda (t: T).(ty3 g c0
+(TSort m) t)) (ty3_sort g c0 m) (lift h d (TSort (next g m))) (lift_sort
+(next g m) h d)) (lift h d (TSort m)) (lift_sort m h d)))))))) (\lambda (n:
+nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c
+(CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u
+t)).(\lambda (H2: ((\forall (c0: C).(\forall (d0: nat).(\forall (h:
+nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u) (lift h d0
+t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h: nat).(\lambda (H3:
+(drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0
+(lift (S n) O t))) (\lambda (H4: (lt n d0)).(let H5 \def (drop_getl_trans_le
+n d0 (le_S_n n d0 (le_S_n (S n) (S d0) (le_S (S (S n)) (S d0) (le_n_S (S n)
+d0 H4)))) c0 c h H3 (CHead d (Bind Abbr) u) H0) in (ex3_2_ind C C (\lambda
+(e0: C).(\lambda (_: C).(drop n O c0 e0))) (\lambda (e0: C).(\lambda (e1:
+C).(drop h (minus d0 n) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1
+(CHead d (Bind Abbr) u)))) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift
+(S n) O t))) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop n O c0
+x0)).(\lambda (H7: (drop h (minus d0 n) x0 x1)).(\lambda (H8: (clear x1
+(CHead d (Bind Abbr) u))).(let H9 \def (eq_ind nat (minus d0 n) (\lambda (n0:
+nat).(drop h n0 x0 x1)) H7 (S (minus d0 (S n))) (minus_x_Sy d0 n H4)) in (let
+H10 \def (drop_clear_S x1 x0 h (minus d0 (S n)) H9 Abbr d u H8) in (ex2_ind C
+(\lambda (c1: C).(clear x0 (CHead c1 (Bind Abbr) (lift h (minus d0 (S n))
+u)))) (\lambda (c1: C).(drop h (minus d0 (S n)) c1 d)) (ty3 g c0 (lift h d0
+(TLRef n)) (lift h d0 (lift (S n) O t))) (\lambda (x: C).(\lambda (H11:
+(clear x0 (CHead x (Bind Abbr) (lift h (minus d0 (S n)) u)))).(\lambda (H12:
+(drop h (minus d0 (S n)) x d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ty3 g
+c0 t0 (lift h d0 (lift (S n) O t)))) (eq_ind nat (plus (S n) (minus d0 (S
+n))) (\lambda (n0: nat).(ty3 g c0 (TLRef n) (lift h n0 (lift (S n) O t))))
+(eq_ind_r T (lift (S n) O (lift h (minus d0 (S n)) t)) (\lambda (t0: T).(ty3
+g c0 (TLRef n) t0)) (eq_ind nat d0 (\lambda (_: nat).(ty3 g c0 (TLRef n)
+(lift (S n) O (lift h (minus d0 (S n)) t)))) (ty3_abbr g n c0 x (lift h
+(minus d0 (S n)) u) (getl_intro n c0 (CHead x (Bind Abbr) (lift h (minus d0
+(S n)) u)) x0 H6 H11) (lift h (minus d0 (S n)) t) (H2 x (minus d0 (S n)) h
+H12)) (plus (S n) (minus d0 (S n))) (le_plus_minus (S n) d0 H4)) (lift h
+(plus (S n) (minus d0 (S n))) (lift (S n) O t)) (lift_d t h (S n) (minus d0
+(S n)) O (le_O_n (minus d0 (S n))))) d0 (le_plus_minus_r (S n) d0 H4)) (lift
+h d0 (TLRef n)) (lift_lref_lt n h d0 H4))))) H10)))))))) H5))) (\lambda (H4:
+(le d0 n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(ty3 g c0 t0 (lift
+h d0 (lift (S n) O t)))) (eq_ind nat (S n) (\lambda (_: nat).(ty3 g c0 (TLRef
+(plus n h)) (lift h d0 (lift (S n) O t)))) (eq_ind_r T (lift (plus h (S n)) O
+t) (\lambda (t0: T).(ty3 g c0 (TLRef (plus n h)) t0)) (eq_ind_r nat (plus (S
+n) h) (\lambda (n0: nat).(ty3 g c0 (TLRef (plus n h)) (lift n0 O t)))
+(ty3_abbr g (plus n h) c0 d u (drop_getl_trans_ge n c0 c d0 h H3 (CHead d
+(Bind Abbr) u) H0 H4) t H1) (plus h (S n)) (plus_sym h (S n))) (lift h d0
+(lift (S n) O t)) (lift_free t (S n) h O d0 (le_S_n d0 (S n) (le_S (S d0) (S
+n) (le_n_S d0 n H4))) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
+n) (\lambda (n0: nat).(eq nat (S n) n0)) (le_antisym (S n) (plus (S O) n)
+(le_n (plus (S O) n)) (le_n (S n))) (plus n (S O)) (plus_sym n (S O)))) (lift
+h d0 (TLRef n)) (lift_lref_ge n h d0 H4)))))))))))))))) (\lambda (n:
+nat).(\lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c
+(CHead d (Bind Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u
+t)).(\lambda (H2: ((\forall (c0: C).(\forall (d0: nat).(\forall (h:
+nat).((drop h d0 c0 d) \to (ty3 g c0 (lift h d0 u) (lift h d0
+t)))))))).(\lambda (c0: C).(\lambda (d0: nat).(\lambda (h: nat).(\lambda (H3:
+(drop h d0 c0 c)).(lt_le_e n d0 (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0
+(lift (S n) O u))) (\lambda (H4: (lt n d0)).(let H5 \def (drop_getl_trans_le
+n d0 (le_S_n n d0 (le_S_n (S n) (S d0) (le_S (S (S n)) (S d0) (le_n_S (S n)
+d0 H4)))) c0 c h H3 (CHead d (Bind Abst) u) H0) in (ex3_2_ind C C (\lambda
+(e0: C).(\lambda (_: C).(drop n O c0 e0))) (\lambda (e0: C).(\lambda (e1:
+C).(drop h (minus d0 n) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear e1
+(CHead d (Bind Abst) u)))) (ty3 g c0 (lift h d0 (TLRef n)) (lift h d0 (lift
+(S n) O u))) (\lambda (x0: C).(\lambda (x1: C).(\lambda (H6: (drop n O c0
+x0)).(\lambda (H7: (drop h (minus d0 n) x0 x1)).(\lambda (H8: (clear x1
+(CHead d (Bind Abst) u))).(let H9 \def (eq_ind nat (minus d0 n) (\lambda (n0:
+nat).(drop h n0 x0 x1)) H7 (S (minus d0 (S n))) (minus_x_Sy d0 n H4)) in (let
+H10 \def (drop_clear_S x1 x0 h (minus d0 (S n)) H9 Abst d u H8) in (ex2_ind C
+(\lambda (c1: C).(clear x0 (CHead c1 (Bind Abst) (lift h (minus d0 (S n))
+u)))) (\lambda (c1: C).(drop h (minus d0 (S n)) c1 d)) (ty3 g c0 (lift h d0
+(TLRef n)) (lift h d0 (lift (S n) O u))) (\lambda (x: C).(\lambda (H11:
+(clear x0 (CHead x (Bind Abst) (lift h (minus d0 (S n)) u)))).(\lambda (H12:
+(drop h (minus d0 (S n)) x d)).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ty3 g
+c0 t0 (lift h d0 (lift (S n) O u)))) (eq_ind nat (plus (S n) (minus d0 (S
+n))) (\lambda (n0: nat).(ty3 g c0 (TLRef n) (lift h n0 (lift (S n) O u))))
+(eq_ind_r T (lift (S n) O (lift h (minus d0 (S n)) u)) (\lambda (t0: T).(ty3
+g c0 (TLRef n) t0)) (eq_ind nat d0 (\lambda (_: nat).(ty3 g c0 (TLRef n)
+(lift (S n) O (lift h (minus d0 (S n)) u)))) (ty3_abst g n c0 x (lift h
+(minus d0 (S n)) u) (getl_intro n c0 (CHead x (Bind Abst) (lift h (minus d0
+(S n)) u)) x0 H6 H11) (lift h (minus d0 (S n)) t) (H2 x (minus d0 (S n)) h
+H12)) (plus (S n) (minus d0 (S n))) (le_plus_minus (S n) d0 H4)) (lift h
+(plus (S n) (minus d0 (S n))) (lift (S n) O u)) (lift_d u h (S n) (minus d0
+(S n)) O (le_O_n (minus d0 (S n))))) d0 (le_plus_minus_r (S n) d0 H4)) (lift
+h d0 (TLRef n)) (lift_lref_lt n h d0 H4))))) H10)))))))) H5))) (\lambda (H4:
+(le d0 n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(ty3 g c0 t0 (lift
+h d0 (lift (S n) O u)))) (eq_ind nat (S n) (\lambda (_: nat).(ty3 g c0 (TLRef
+(plus n h)) (lift h d0 (lift (S n) O u)))) (eq_ind_r T (lift (plus h (S n)) O
+u) (\lambda (t0: T).(ty3 g c0 (TLRef (plus n h)) t0)) (eq_ind_r nat (plus (S
+n) h) (\lambda (n0: nat).(ty3 g c0 (TLRef (plus n h)) (lift n0 O u)))
+(ty3_abst g (plus n h) c0 d u (drop_getl_trans_ge n c0 c d0 h H3 (CHead d
+(Bind Abst) u) H0 H4) t H1) (plus h (S n)) (plus_sym h (S n))) (lift h d0
+(lift (S n) O u)) (lift_free u (S n) h O d0 (le_S_n d0 (S n) (le_S (S d0) (S
+n) (le_n_S d0 n H4))) (le_O_n d0))) (plus n (S O)) (eq_ind_r nat (plus (S O)
+n) (\lambda (n0: nat).(eq nat (S n) n0)) (le_antisym (S n) (plus (S O) n)
+(le_n (plus (S O) n)) (le_n (S n))) (plus n (S O)) (plus_sym n (S O)))) (lift
+h d0 (TLRef n)) (lift_lref_ge n h d0 H4)))))))))))))))) (\lambda (c:
+C).(\lambda (u: T).(\lambda (t: T).(\lambda (_: (ty3 g c u t)).(\lambda (H1:
+((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to
+(ty3 g c0 (lift h d u) (lift h d t)))))))).(\lambda (b: B).(\lambda (t0:
+T).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c (Bind b) u) t0 t3)).(\lambda
+(H3: ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0
+(CHead c (Bind b) u)) \to (ty3 g c0 (lift h d t0) (lift h d
+t3)))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4:
+(drop h d c0 c)).(eq_ind_r T (THead (Bind b) (lift h d u) (lift h (s (Bind b)
+d) t0)) (\lambda (t4: T).(ty3 g c0 t4 (lift h d (THead (Bind b) u t3))))
+(eq_ind_r T (THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t3)) (\lambda
+(t4: T).(ty3 g c0 (THead (Bind b) (lift h d u) (lift h (s (Bind b) d) t0))
+t4)) (ty3_bind g c0 (lift h d u) (lift h d t) (H1 c0 d h H4) b (lift h (S d)
+t0) (lift h (S d) t3) (H3 (CHead c0 (Bind b) (lift h d u)) (S d) h
+(drop_skip_bind h d c0 c H4 b u))) (lift h d (THead (Bind b) u t3))
+(lift_head (Bind b) u t3 h d)) (lift h d (THead (Bind b) u t0)) (lift_head
+(Bind b) u t0 h d)))))))))))))))) (\lambda (c: C).(\lambda (w: T).(\lambda
+(u: T).(\lambda (_: (ty3 g c w u)).(\lambda (H1: ((\forall (c0: C).(\forall
+(d: nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d w) (lift
+h d u)))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c v (THead
+(Bind Abst) u t))).(\lambda (H3: ((\forall (c0: C).(\forall (d: nat).(\forall
+(h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d v) (lift h d (THead (Bind
+Abst) u t))))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h:
+nat).(\lambda (H4: (drop h d c0 c)).(eq_ind_r T (THead (Flat Appl) (lift h d
+w) (lift h (s (Flat Appl) d) v)) (\lambda (t0: T).(ty3 g c0 t0 (lift h d
+(THead (Flat Appl) w (THead (Bind Abst) u t))))) (eq_ind_r T (THead (Flat
+Appl) (lift h d w) (lift h (s (Flat Appl) d) (THead (Bind Abst) u t)))
+(\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) (lift h d w) (lift h (s (Flat
+Appl) d) v)) t0)) (eq_ind_r T (THead (Bind Abst) (lift h (s (Flat Appl) d) u)
+(lift h (s (Bind Abst) (s (Flat Appl) d)) t)) (\lambda (t0: T).(ty3 g c0
+(THead (Flat Appl) (lift h d w) (lift h (s (Flat Appl) d) v)) (THead (Flat
+Appl) (lift h d w) t0))) (ty3_appl g c0 (lift h d w) (lift h d u) (H1 c0 d h
+H4) (lift h d v) (lift h (S d) t) (eq_ind T (lift h d (THead (Bind Abst) u
+t)) (\lambda (t0: T).(ty3 g c0 (lift h d v) t0)) (H3 c0 d h H4) (THead (Bind
+Abst) (lift h d u) (lift h (S d) t)) (lift_bind Abst u t h d))) (lift h (s
+(Flat Appl) d) (THead (Bind Abst) u t)) (lift_head (Bind Abst) u t h (s (Flat
+Appl) d))) (lift h d (THead (Flat Appl) w (THead (Bind Abst) u t)))
+(lift_head (Flat Appl) w (THead (Bind Abst) u t) h d)) (lift h d (THead (Flat
+Appl) w v)) (lift_head (Flat Appl) w v h d))))))))))))))) (\lambda (c:
+C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (ty3 g c t0 t3)).(\lambda
+(H1: ((\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c)
+\to (ty3 g c0 (lift h d t0) (lift h d t3)))))))).(\lambda (t4: T).(\lambda
+(_: (ty3 g c t3 t4)).(\lambda (H3: ((\forall (c0: C).(\forall (d:
+nat).(\forall (h: nat).((drop h d c0 c) \to (ty3 g c0 (lift h d t3) (lift h d