- \lambda (t1: T).(let TMP_5 \def (\lambda (t: T).(\forall (x: T).(\forall
-(h1: nat).(\forall (h2: nat).(\forall (d1: nat).(\forall (d2: nat).((le d1
-d2) \to ((eq T (lift h1 d1 t) (lift h2 (plus d2 h1) x)) \to (let TMP_2 \def
-(\lambda (t2: T).(let TMP_1 \def (lift h1 d1 t2) in (eq T x TMP_1))) in (let
-TMP_4 \def (\lambda (t2: T).(let TMP_3 \def (lift h2 d2 t2) in (eq T t
-TMP_3))) in (ex2 T TMP_2 TMP_4))))))))))) in (let TMP_48 \def (\lambda (n:
-nat).(\lambda (x: T).(\lambda (h1: nat).(\lambda (h2: nat).(\lambda (d1:
-nat).(\lambda (d2: nat).(\lambda (_: (le d1 d2)).(\lambda (H0: (eq T (lift h1
-d1 (TSort n)) (lift h2 (plus d2 h1) x))).(let TMP_6 \def (TSort n) in (let
-TMP_7 \def (lift h1 d1 TMP_6) in (let TMP_10 \def (\lambda (t: T).(let TMP_8
-\def (plus d2 h1) in (let TMP_9 \def (lift h2 TMP_8 x) in (eq T t TMP_9))))
-in (let TMP_11 \def (TSort n) in (let TMP_12 \def (lift_sort n h1 d1) in (let
-H1 \def (eq_ind T TMP_7 TMP_10 H0 TMP_11 TMP_12) in (let TMP_13 \def (TSort
-n) in (let TMP_19 \def (\lambda (t: T).(let TMP_15 \def (\lambda (t2: T).(let
-TMP_14 \def (lift h1 d1 t2) in (eq T t TMP_14))) in (let TMP_18 \def (\lambda
-(t2: T).(let TMP_16 \def (TSort n) in (let TMP_17 \def (lift h2 d2 t2) in (eq
-T TMP_16 TMP_17)))) in (ex2 T TMP_15 TMP_18)))) in (let TMP_22 \def (\lambda
-(t2: T).(let TMP_20 \def (TSort n) in (let TMP_21 \def (lift h1 d1 t2) in (eq
-T TMP_20 TMP_21)))) in (let TMP_25 \def (\lambda (t2: T).(let TMP_23 \def
-(TSort n) in (let TMP_24 \def (lift h2 d2 t2) in (eq T TMP_23 TMP_24)))) in
-(let TMP_26 \def (TSort n) in (let TMP_27 \def (TSort n) in (let TMP_29 \def
-(\lambda (t: T).(let TMP_28 \def (TSort n) in (eq T TMP_28 t))) in (let
-TMP_30 \def (TSort n) in (let TMP_31 \def (refl_equal T TMP_30) in (let
-TMP_32 \def (TSort n) in (let TMP_33 \def (lift h1 d1 TMP_32) in (let TMP_34
-\def (lift_sort n h1 d1) in (let TMP_35 \def (eq_ind_r T TMP_27 TMP_29 TMP_31
-TMP_33 TMP_34) in (let TMP_36 \def (TSort n) in (let TMP_38 \def (\lambda (t:
-T).(let TMP_37 \def (TSort n) in (eq T TMP_37 t))) in (let TMP_39 \def (TSort
-n) in (let TMP_40 \def (refl_equal T TMP_39) in (let TMP_41 \def (TSort n) in
-(let TMP_42 \def (lift h2 d2 TMP_41) in (let TMP_43 \def (lift_sort n h2 d2)
-in (let TMP_44 \def (eq_ind_r T TMP_36 TMP_38 TMP_40 TMP_42 TMP_43) in (let
-TMP_45 \def (ex_intro2 T TMP_22 TMP_25 TMP_26 TMP_35 TMP_44) in (let TMP_46
-\def (plus d2 h1) in (let TMP_47 \def (lift_gen_sort h2 TMP_46 n x H1) in
-(eq_ind_r T TMP_13 TMP_19 TMP_45 x
-TMP_47))))))))))))))))))))))))))))))))))))))) in (let TMP_325 \def (\lambda
-(n: nat).(\lambda (x: T).(\lambda (h1: nat).(\lambda (h2: nat).(\lambda (d1:
-nat).(\lambda (d2: nat).(\lambda (H: (le d1 d2)).(\lambda (H0: (eq T (lift h1
-d1 (TLRef n)) (lift h2 (plus d2 h1) x))).(let TMP_50 \def (\lambda (t2:
-T).(let TMP_49 \def (lift h1 d1 t2) in (eq T x TMP_49))) in (let TMP_53 \def
-(\lambda (t2: T).(let TMP_51 \def (TLRef n) in (let TMP_52 \def (lift h2 d2
-t2) in (eq T TMP_51 TMP_52)))) in (let TMP_54 \def (ex2 T TMP_50 TMP_53) in
-(let TMP_101 \def (\lambda (H1: (lt n d1)).(let TMP_55 \def (TLRef n) in (let
-TMP_56 \def (lift h1 d1 TMP_55) in (let TMP_59 \def (\lambda (t: T).(let
-TMP_57 \def (plus d2 h1) in (let TMP_58 \def (lift h2 TMP_57 x) in (eq T t
-TMP_58)))) in (let TMP_60 \def (TLRef n) in (let TMP_61 \def (lift_lref_lt n
-h1 d1 H1) in (let H2 \def (eq_ind T TMP_56 TMP_59 H0 TMP_60 TMP_61) in (let
-TMP_62 \def (TLRef n) in (let TMP_68 \def (\lambda (t: T).(let TMP_64 \def
-(\lambda (t2: T).(let TMP_63 \def (lift h1 d1 t2) in (eq T t TMP_63))) in
-(let TMP_67 \def (\lambda (t2: T).(let TMP_65 \def (TLRef n) in (let TMP_66
-\def (lift h2 d2 t2) in (eq T TMP_65 TMP_66)))) in (ex2 T TMP_64 TMP_67))))
-in (let TMP_71 \def (\lambda (t2: T).(let TMP_69 \def (TLRef n) in (let
-TMP_70 \def (lift h1 d1 t2) in (eq T TMP_69 TMP_70)))) in (let TMP_74 \def
-(\lambda (t2: T).(let TMP_72 \def (TLRef n) in (let TMP_73 \def (lift h2 d2
-t2) in (eq T TMP_72 TMP_73)))) in (let TMP_75 \def (TLRef n) in (let TMP_76
-\def (TLRef n) in (let TMP_78 \def (\lambda (t: T).(let TMP_77 \def (TLRef n)
-in (eq T TMP_77 t))) in (let TMP_79 \def (TLRef n) in (let TMP_80 \def
-(refl_equal T TMP_79) in (let TMP_81 \def (TLRef n) in (let TMP_82 \def (lift
-h1 d1 TMP_81) in (let TMP_83 \def (lift_lref_lt n h1 d1 H1) in (let TMP_84
-\def (eq_ind_r T TMP_76 TMP_78 TMP_80 TMP_82 TMP_83) in (let TMP_85 \def
-(TLRef n) in (let TMP_87 \def (\lambda (t: T).(let TMP_86 \def (TLRef n) in
-(eq T TMP_86 t))) in (let TMP_88 \def (TLRef n) in (let TMP_89 \def
-(refl_equal T TMP_88) in (let TMP_90 \def (TLRef n) in (let TMP_91 \def (lift
-h2 d2 TMP_90) in (let TMP_92 \def (lt_le_trans n d1 d2 H1 H) in (let TMP_93
-\def (lift_lref_lt n h2 d2 TMP_92) in (let TMP_94 \def (eq_ind_r T TMP_85
-TMP_87 TMP_89 TMP_91 TMP_93) in (let TMP_95 \def (ex_intro2 T TMP_71 TMP_74
-TMP_75 TMP_84 TMP_94) in (let TMP_96 \def (plus d2 h1) in (let TMP_97 \def
-(plus d2 h1) in (let TMP_98 \def (le_plus_trans d1 d2 h1 H) in (let TMP_99
-\def (lt_le_trans n d1 TMP_97 H1 TMP_98) in (let TMP_100 \def
-(lift_gen_lref_lt h2 TMP_96 n TMP_99 x H2) in (eq_ind_r T TMP_62 TMP_68
-TMP_95 x TMP_100)))))))))))))))))))))))))))))))))))) in (let TMP_324 \def
-(\lambda (H1: (le d1 n)).(let TMP_102 \def (TLRef n) in (let TMP_103 \def
-(lift h1 d1 TMP_102) in (let TMP_106 \def (\lambda (t: T).(let TMP_104 \def
-(plus d2 h1) in (let TMP_105 \def (lift h2 TMP_104 x) in (eq T t TMP_105))))
-in (let TMP_107 \def (plus n h1) in (let TMP_108 \def (TLRef TMP_107) in (let
-TMP_109 \def (lift_lref_ge n h1 d1 H1) in (let H2 \def (eq_ind T TMP_103
-TMP_106 H0 TMP_108 TMP_109) in (let TMP_111 \def (\lambda (t2: T).(let
-TMP_110 \def (lift h1 d1 t2) in (eq T x TMP_110))) in (let TMP_114 \def
-(\lambda (t2: T).(let TMP_112 \def (TLRef n) in (let TMP_113 \def (lift h2 d2
-t2) in (eq T TMP_112 TMP_113)))) in (let TMP_115 \def (ex2 T TMP_111 TMP_114)
-in (let TMP_158 \def (\lambda (H3: (lt n d2)).(let TMP_116 \def (plus n h1)
-in (let TMP_117 \def (TLRef TMP_116) in (let TMP_123 \def (\lambda (t:
-T).(let TMP_119 \def (\lambda (t2: T).(let TMP_118 \def (lift h1 d1 t2) in
-(eq T t TMP_118))) in (let TMP_122 \def (\lambda (t2: T).(let TMP_120 \def
-(TLRef n) in (let TMP_121 \def (lift h2 d2 t2) in (eq T TMP_120 TMP_121))))
-in (ex2 T TMP_119 TMP_122)))) in (let TMP_127 \def (\lambda (t2: T).(let
-TMP_124 \def (plus n h1) in (let TMP_125 \def (TLRef TMP_124) in (let TMP_126
-\def (lift h1 d1 t2) in (eq T TMP_125 TMP_126))))) in (let TMP_130 \def
-(\lambda (t2: T).(let TMP_128 \def (TLRef n) in (let TMP_129 \def (lift h2 d2
-t2) in (eq T TMP_128 TMP_129)))) in (let TMP_131 \def (TLRef n) in (let
-TMP_132 \def (plus n h1) in (let TMP_133 \def (TLRef TMP_132) in (let TMP_136
-\def (\lambda (t: T).(let TMP_134 \def (plus n h1) in (let TMP_135 \def
-(TLRef TMP_134) in (eq T TMP_135 t)))) in (let TMP_137 \def (plus n h1) in
-(let TMP_138 \def (TLRef TMP_137) in (let TMP_139 \def (refl_equal T TMP_138)
-in (let TMP_140 \def (TLRef n) in (let TMP_141 \def (lift h1 d1 TMP_140) in
-(let TMP_142 \def (lift_lref_ge n h1 d1 H1) in (let TMP_143 \def (eq_ind_r T
-TMP_133 TMP_136 TMP_139 TMP_141 TMP_142) in (let TMP_144 \def (TLRef n) in
-(let TMP_146 \def (\lambda (t: T).(let TMP_145 \def (TLRef n) in (eq T
-TMP_145 t))) in (let TMP_147 \def (TLRef n) in (let TMP_148 \def (refl_equal
-T TMP_147) in (let TMP_149 \def (TLRef n) in (let TMP_150 \def (lift h2 d2
-TMP_149) in (let TMP_151 \def (lift_lref_lt n h2 d2 H3) in (let TMP_152 \def
-(eq_ind_r T TMP_144 TMP_146 TMP_148 TMP_150 TMP_151) in (let TMP_153 \def
-(ex_intro2 T TMP_127 TMP_130 TMP_131 TMP_143 TMP_152) in (let TMP_154 \def
-(plus d2 h1) in (let TMP_155 \def (plus n h1) in (let TMP_156 \def (lt_reg_r
-n d2 h1 H3) in (let TMP_157 \def (lift_gen_lref_lt h2 TMP_154 TMP_155 TMP_156
-x H2) in (eq_ind_r T TMP_117 TMP_123 TMP_153 x
-TMP_157))))))))))))))))))))))))))))))) in (let TMP_323 \def (\lambda (H3: (le
-d2 n)).(let TMP_159 \def (plus d2 h2) in (let TMP_161 \def (\lambda (t2:
-T).(let TMP_160 \def (lift h1 d1 t2) in (eq T x TMP_160))) in (let TMP_164
-\def (\lambda (t2: T).(let TMP_162 \def (TLRef n) in (let TMP_163 \def (lift
-h2 d2 t2) in (eq T TMP_162 TMP_163)))) in (let TMP_165 \def (ex2 T TMP_161
-TMP_164) in (let TMP_186 \def (\lambda (H4: (lt n (plus d2 h2))).(let TMP_166
-\def (plus d2 h1) in (let TMP_167 \def (plus n h1) in (let TMP_168 \def (le_n
-h1) in (let TMP_169 \def (le_plus_plus d2 n h1 h1 H3 TMP_168) in (let TMP_170
-\def (plus d2 h2) in (let TMP_171 \def (plus TMP_170 h1) in (let TMP_173 \def
-(\lambda (n0: nat).(let TMP_172 \def (plus n h1) in (lt TMP_172 n0))) in (let
-TMP_174 \def (plus d2 h2) in (let TMP_175 \def (lt_reg_r n TMP_174 h1 H4) in
-(let TMP_176 \def (plus d2 h1) in (let TMP_177 \def (plus TMP_176 h2) in (let
-TMP_178 \def (plus_permute_2_in_3 d2 h1 h2) in (let TMP_179 \def (eq_ind_r
-nat TMP_171 TMP_173 TMP_175 TMP_177 TMP_178) in (let TMP_181 \def (\lambda
-(t2: T).(let TMP_180 \def (lift h1 d1 t2) in (eq T x TMP_180))) in (let
-TMP_184 \def (\lambda (t2: T).(let TMP_182 \def (TLRef n) in (let TMP_183
-\def (lift h2 d2 t2) in (eq T TMP_182 TMP_183)))) in (let TMP_185 \def (ex2 T
-TMP_181 TMP_184) in (lift_gen_lref_false h2 TMP_166 TMP_167 TMP_169 TMP_179 x
-H2 TMP_185)))))))))))))))))) in (let TMP_322 \def (\lambda (H4: (le (plus d2
-h2) n)).(let TMP_187 \def (plus n h1) in (let TMP_191 \def (\lambda (n0:
-nat).(let TMP_188 \def (TLRef n0) in (let TMP_189 \def (plus d2 h1) in (let
-TMP_190 \def (lift h2 TMP_189 x) in (eq T TMP_188 TMP_190))))) in (let
-TMP_192 \def (plus n h1) in (let TMP_193 \def (minus TMP_192 h2) in (let
-TMP_194 \def (plus TMP_193 h2) in (let TMP_195 \def (plus n h1) in (let
-TMP_196 \def (plus d2 h2) in (let TMP_197 \def (le_plus_r d2 h2) in (let
-TMP_198 \def (le_trans h2 TMP_196 n TMP_197 H4) in (let TMP_199 \def
-(le_plus_trans h2 n h1 TMP_198) in (let TMP_200 \def (le_plus_minus_sym h2
-TMP_195 TMP_199) in (let H5 \def (eq_ind nat TMP_187 TMP_191 H2 TMP_194
-TMP_200) in (let TMP_201 \def (plus n h1) in (let TMP_202 \def (minus TMP_201
-h2) in (let TMP_203 \def (TLRef TMP_202) in (let TMP_209 \def (\lambda (t:
-T).(let TMP_205 \def (\lambda (t2: T).(let TMP_204 \def (lift h1 d1 t2) in
-(eq T t TMP_204))) in (let TMP_208 \def (\lambda (t2: T).(let TMP_206 \def
-(TLRef n) in (let TMP_207 \def (lift h2 d2 t2) in (eq T TMP_206 TMP_207))))
-in (ex2 T TMP_205 TMP_208)))) in (let TMP_214 \def (\lambda (t2: T).(let
-TMP_210 \def (plus n h1) in (let TMP_211 \def (minus TMP_210 h2) in (let
-TMP_212 \def (TLRef TMP_211) in (let TMP_213 \def (lift h1 d1 t2) in (eq T
-TMP_212 TMP_213)))))) in (let TMP_217 \def (\lambda (t2: T).(let TMP_215 \def
-(TLRef n) in (let TMP_216 \def (lift h2 d2 t2) in (eq T TMP_215 TMP_216))))
-in (let TMP_218 \def (minus n h2) in (let TMP_219 \def (TLRef TMP_218) in
-(let TMP_220 \def (minus n h2) in (let TMP_221 \def (plus TMP_220 h1) in (let
-TMP_226 \def (\lambda (n0: nat).(let TMP_222 \def (TLRef n0) in (let TMP_223
-\def (minus n h2) in (let TMP_224 \def (TLRef TMP_223) in (let TMP_225 \def
-(lift h1 d1 TMP_224) in (eq T TMP_222 TMP_225)))))) in (let TMP_227 \def
-(minus n h2) in (let TMP_228 \def (plus TMP_227 h1) in (let TMP_229 \def
-(TLRef TMP_228) in (let TMP_233 \def (\lambda (t: T).(let TMP_230 \def (minus
-n h2) in (let TMP_231 \def (plus TMP_230 h1) in (let TMP_232 \def (TLRef
-TMP_231) in (eq T TMP_232 t))))) in (let TMP_234 \def (minus n h2) in (let
-TMP_235 \def (plus TMP_234 h1) in (let TMP_236 \def (TLRef TMP_235) in (let
-TMP_237 \def (refl_equal T TMP_236) in (let TMP_238 \def (minus n h2) in (let
-TMP_239 \def (TLRef TMP_238) in (let TMP_240 \def (lift h1 d1 TMP_239) in
-(let TMP_241 \def (minus n h2) in (let TMP_242 \def (minus n h2) in (let
-TMP_243 \def (le_minus d2 n h2 H4) in (let TMP_244 \def (le_trans d1 d2
-TMP_242 H TMP_243) in (let TMP_245 \def (lift_lref_ge TMP_241 h1 d1 TMP_244)
-in (let TMP_246 \def (eq_ind_r T TMP_229 TMP_233 TMP_237 TMP_240 TMP_245) in
-(let TMP_247 \def (plus n h1) in (let TMP_248 \def (minus TMP_247 h2) in (let
-TMP_249 \def (plus d2 h2) in (let TMP_250 \def (le_plus_r d2 h2) in (let
-TMP_251 \def (le_trans h2 TMP_249 n TMP_250 H4) in (let TMP_252 \def
-(le_minus_plus h2 n TMP_251 h1) in (let TMP_253 \def (eq_ind_r nat TMP_221
-TMP_226 TMP_246 TMP_248 TMP_252) in (let TMP_254 \def (minus n h2) in (let
-TMP_255 \def (plus TMP_254 h2) in (let TMP_260 \def (\lambda (n0: nat).(let
-TMP_256 \def (TLRef n0) in (let TMP_257 \def (minus n0 h2) in (let TMP_258
-\def (TLRef TMP_257) in (let TMP_259 \def (lift h2 d2 TMP_258) in (eq T
-TMP_256 TMP_259)))))) in (let TMP_261 \def (minus n h2) in (let TMP_262 \def
-(plus TMP_261 h2) in (let TMP_263 \def (minus TMP_262 h2) in (let TMP_264
-\def (plus TMP_263 h2) in (let TMP_265 \def (TLRef TMP_264) in (let TMP_269
-\def (\lambda (t: T).(let TMP_266 \def (minus n h2) in (let TMP_267 \def
-(plus TMP_266 h2) in (let TMP_268 \def (TLRef TMP_267) in (eq T TMP_268
-t))))) in (let TMP_270 \def (minus n h2) in (let TMP_271 \def (plus TMP_270
-h2) in (let TMP_272 \def (minus TMP_271 h2) in (let TMP_273 \def (plus
-TMP_272 h2) in (let TMP_274 \def (TLRef TMP_273) in (let TMP_275 \def (minus
-n h2) in (let TMP_276 \def (plus TMP_275 h2) in (let TMP_277 \def (TLRef
-TMP_276) in (let TMP_278 \def (minus n h2) in (let TMP_279 \def (plus TMP_278
-h2) in (let TMP_280 \def (minus TMP_279 h2) in (let TMP_281 \def (plus
-TMP_280 h2) in (let TMP_282 \def (minus n h2) in (let TMP_283 \def (plus
-TMP_282 h2) in (let TMP_284 \def (minus n h2) in (let TMP_285 \def (plus
-TMP_284 h2) in (let TMP_286 \def (minus TMP_285 h2) in (let TMP_287 \def
-(minus n h2) in (let TMP_288 \def (minus n h2) in (let TMP_289 \def
-(minus_plus_r TMP_288 h2) in (let TMP_290 \def (refl_equal nat h2) in (let
-TMP_291 \def (f_equal2 nat nat nat plus TMP_286 TMP_287 h2 h2 TMP_289
-TMP_290) in (let TMP_292 \def (f_equal nat T TLRef TMP_281 TMP_283 TMP_291)
-in (let TMP_293 \def (sym_eq T TMP_274 TMP_277 TMP_292) in (let TMP_294 \def
-(minus n h2) in (let TMP_295 \def (plus TMP_294 h2) in (let TMP_296 \def
-(minus TMP_295 h2) in (let TMP_297 \def (TLRef TMP_296) in (let TMP_298 \def
-(lift h2 d2 TMP_297) in (let TMP_299 \def (minus n h2) in (let TMP_300 \def
-(plus TMP_299 h2) in (let TMP_301 \def (minus TMP_300 h2) in (let TMP_302
-\def (minus n h2) in (let TMP_303 \def (plus TMP_302 h2) in (let TMP_304 \def
-(minus n h2) in (let TMP_305 \def (le_minus d2 n h2 H4) in (let TMP_306 \def
-(le_n h2) in (let TMP_307 \def (le_plus_plus d2 TMP_304 h2 h2 TMP_305
-TMP_306) in (let TMP_308 \def (le_minus d2 TMP_303 h2 TMP_307) in (let
-TMP_309 \def (lift_lref_ge TMP_301 h2 d2 TMP_308) in (let TMP_310 \def
-(eq_ind_r T TMP_265 TMP_269 TMP_293 TMP_298 TMP_309) in (let TMP_311 \def
-(plus d2 h2) in (let TMP_312 \def (le_plus_r d2 h2) in (let TMP_313 \def
-(le_trans h2 TMP_311 n TMP_312 H4) in (let TMP_314 \def (le_plus_minus_sym h2
-n TMP_313) in (let TMP_315 \def (eq_ind_r nat TMP_255 TMP_260 TMP_310 n
-TMP_314) in (let TMP_316 \def (ex_intro2 T TMP_214 TMP_217 TMP_219 TMP_253
-TMP_315) in (let TMP_317 \def (plus d2 h1) in (let TMP_318 \def (plus n h1)
-in (let TMP_319 \def (minus TMP_318 h2) in (let TMP_320 \def (arith0 h2 d2 n
-H4 h1) in (let TMP_321 \def (lift_gen_lref_ge h2 TMP_317 TMP_319 TMP_320 x
-H5) in (eq_ind_r T TMP_203 TMP_209 TMP_316 x
-TMP_321)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-))))))))))))))))))))))))))))))))))))))) in (lt_le_e n TMP_159 TMP_165 TMP_186
-TMP_322)))))))) in (lt_le_e n d2 TMP_115 TMP_158 TMP_323)))))))))))))) in
-(lt_le_e n d1 TMP_54 TMP_101 TMP_324)))))))))))))) in (let TMP_720 \def
-(\lambda (k: K).(\lambda (t: T).(\lambda (H: ((\forall (x: T).(\forall (h1: