X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fty3%2Fprops.ma;h=d9a82d40e8e8f5bb8c1600b44374616d6c3eb978;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=eedc5fddd81aee725a1767fafdd97382c55adc0f;hpb=10c836687dfdf9d23357d7423cfc535e817d843f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/ty3/props.ma b/matita/matita/contribs/lambdadelta/basic_1/ty3/props.ma
index eedc5fddd..d9a82d40e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/ty3/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/ty3/props.ma
@@ -18,814 +18,404 @@ include "basic_1/ty3/fwd.ma".
 
 include "basic_1/pc3/fwd.ma".
 
-theorem ty3_lift:
+lemma ty3_lift:
  \forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((ty3 g e 
 t1 t2) \to (\forall (c: C).(\forall (d: nat).(\forall (h: nat).((drop h d c 
 e) \to (ty3 g c (lift h d t1) (lift h d t2))))))))))
 \def
  \lambda (g: G).(\lambda (e: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
-(H: (ty3 g e t1 t2)).(let TMP_3 \def (\lambda (c: C).(\lambda (t: T).(\lambda 
-(t0: T).(\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) 
-\to (let TMP_1 \def (lift h d t) in (let TMP_2 \def (lift h d t0) in (ty3 g 
-c0 TMP_1 TMP_2)))))))))) in (let TMP_11 \def (\lambda (c: C).(\lambda (t0: 
+(H: (ty3 g e t1 t2)).(ty3_ind g (\lambda (c: C).(\lambda (t: T).(\lambda (t0: 
+T).(\forall (c0: C).(\forall (d: nat).(\forall (h: nat).((drop h d c0 c) \to 
+(ty3 g c0 (lift h d t) (lift h d t0))))))))) (\lambda (c: C).(\lambda (t0: 
 T).(\lambda (t: T).(\lambda (_: (ty3 g c t0 t)).(\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 t)))))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (_: (ty3 
 g c u t3)).(\lambda (H3: ((\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 
 t3)))))))).(\lambda (H4: (pc3 c t3 t0)).(\lambda (c0: C).(\lambda (d: 
-nat).(\lambda (h: nat).(\lambda (H5: (drop h d c0 c)).(let TMP_4 \def (lift h 
-d t0) in (let TMP_5 \def (lift h d t) in (let TMP_6 \def (H1 c0 d h H5) in 
-(let TMP_7 \def (lift h d u) in (let TMP_8 \def (lift h d t3) in (let TMP_9 
-\def (H3 c0 d h H5) in (let TMP_10 \def (pc3_lift c0 c h d H5 t3 t0 H4) in 
-(ty3_conv g c0 TMP_4 TMP_5 TMP_6 TMP_7 TMP_8 TMP_9 
-TMP_10)))))))))))))))))))))) in (let TMP_31 \def (\lambda (c: C).(\lambda (m: 
+nat).(\lambda (h: nat).(\lambda (H5: (drop h d c0 c)).(ty3_conv g c0 (lift h 
+d t0) (lift h d t) (H1 c0 d h H5) (lift h d u) (lift h d t3) (H3 c0 d h H5) 
+(pc3_lift c0 c h d H5 t3 t0 H4)))))))))))))))) (\lambda (c: C).(\lambda (m: 
 nat).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (_: (drop 
-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 
 t4)))))))).(\lambda (c0: C).(\lambda (d: nat).(\lambda (h: nat).(\lambda (H4: 
-(drop h d c0 c)).(let TMP_578 \def (Flat Cast) in (let TMP_579 \def (lift h d 
-t3) in (let TMP_580 \def (Flat Cast) in (let TMP_581 \def (s TMP_580 d) in 
-(let TMP_582 \def (lift h TMP_581 t0) in (let TMP_583 \def (THead TMP_578 
-TMP_579 TMP_582) in (let TMP_587 \def (\lambda (t: T).(let TMP_584 \def (Flat 
-Cast) in (let TMP_585 \def (THead TMP_584 t4 t3) in (let TMP_586 \def (lift h 
-d TMP_585) in (ty3 g c0 t TMP_586))))) in (let TMP_588 \def (Flat Cast) in 
-(let TMP_589 \def (lift h d t4) in (let TMP_590 \def (Flat Cast) in (let 
-TMP_591 \def (s TMP_590 d) in (let TMP_592 \def (lift h TMP_591 t3) in (let 
-TMP_593 \def (THead TMP_588 TMP_589 TMP_592) in (let TMP_600 \def (\lambda 
-(t: T).(let TMP_594 \def (Flat Cast) in (let TMP_595 \def (lift h d t3) in 
-(let TMP_596 \def (Flat Cast) in (let TMP_597 \def (s TMP_596 d) in (let 
-TMP_598 \def (lift h TMP_597 t0) in (let TMP_599 \def (THead TMP_594 TMP_595 
-TMP_598) in (ty3 g c0 TMP_599 t)))))))) in (let TMP_601 \def (Flat Cast) in 
-(let TMP_602 \def (s TMP_601 d) in (let TMP_603 \def (lift h TMP_602 t0) in 
-(let TMP_604 \def (Flat Cast) in (let TMP_605 \def (s TMP_604 d) in (let 
-TMP_606 \def (lift h TMP_605 t3) in (let TMP_607 \def (Flat Cast) in (let 
-TMP_608 \def (s TMP_607 d) in (let TMP_609 \def (H1 c0 TMP_608 h H4) in (let 
-TMP_610 \def (lift h d t4) in (let TMP_611 \def (H3 c0 d h H4) in (let 
-TMP_612 \def (ty3_cast g c0 TMP_603 TMP_606 TMP_609 TMP_610 TMP_611) in (let 
-TMP_613 \def (Flat Cast) in (let TMP_614 \def (THead TMP_613 t4 t3) in (let 
-TMP_615 \def (lift h d TMP_614) in (let TMP_616 \def (Flat Cast) in (let 
-TMP_617 \def (lift_head TMP_616 t4 t3 h d) in (let TMP_618 \def (eq_ind_r T 
-TMP_593 TMP_600 TMP_612 TMP_615 TMP_617) in (let TMP_619 \def (Flat Cast) in 
-(let TMP_620 \def (THead TMP_619 t3 t0) in (let TMP_621 \def (lift h d 
-TMP_620) in (let TMP_622 \def (Flat Cast) in (let TMP_623 \def (lift_head 
-TMP_622 t3 t0 h d) in (eq_ind_r T TMP_583 TMP_587 TMP_618 TMP_621 
-TMP_623)))))))))))))))))))))))))))))))))))))))))))))))))) in (ty3_ind g TMP_3 
-TMP_11 TMP_31 TMP_233 TMP_435 TMP_484 TMP_577 TMP_624 e t1 t2 H))))))))))))).
+(drop h d c0 c)).(eq_ind_r T (THead (Flat Cast) (lift h d t3) (lift h (s 
+(Flat Cast) d) t0)) (\lambda (t: T).(ty3 g c0 t (lift h d (THead (Flat Cast) 
+t4 t3)))) (eq_ind_r T (THead (Flat Cast) (lift h d t4) (lift h (s (Flat Cast) 
+d) t3)) (\lambda (t: T).(ty3 g c0 (THead (Flat Cast) (lift h d t3) (lift h (s 
+(Flat Cast) d) t0)) t)) (ty3_cast g c0 (lift h (s (Flat Cast) d) t0) (lift h 
+(s (Flat Cast) d) t3) (H1 c0 (s (Flat Cast) d) h H4) (lift h d t4) (H3 c0 d h 
+H4)) (lift h d (THead (Flat Cast) t4 t3)) (lift_head (Flat Cast) t4 t3 h d)) 
+(lift h d (THead (Flat Cast) t3 t0)) (lift_head (Flat Cast) t3 t0 h 
+d)))))))))))))) e t1 t2 H))))).
 
-theorem ty3_correct:
+lemma ty3_correct:
  \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((ty3 g c 
 t1 t2) \to (ex T (\lambda (t: T).(ty3 g c t2 t)))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda 
-(H: (ty3 g c t1 t2)).(let TMP_2 \def (\lambda (c0: C).(\lambda (_: 
-T).(\lambda (t0: T).(let TMP_1 \def (\lambda (t3: T).(ty3 g c0 t0 t3)) in (ex 
-T TMP_1))))) in (let TMP_4 \def (\lambda (c0: C).(\lambda (t0: T).(\lambda 
-(t: T).(\lambda (H0: (ty3 g c0 t0 t)).(\lambda (_: (ex T (\lambda (t3: 
-T).(ty3 g c0 t t3)))).(\lambda (u: T).(\lambda (t3: T).(\lambda (_: (ty3 g c0 
-u t3)).(\lambda (_: (ex T (\lambda (t4: T).(ty3 g c0 t3 t4)))).(\lambda (_: 
-(pc3 c0 t3 t0)).(let TMP_3 \def (\lambda (t4: T).(ty3 g c0 t0 t4)) in 
-(ex_intro T TMP_3 t H0)))))))))))) in (let TMP_13 \def (\lambda (c0: 
-C).(\lambda (m: nat).(let TMP_7 \def (\lambda (t: T).(let TMP_5 \def (next g 
-m) in (let TMP_6 \def (TSort TMP_5) in (ty3 g c0 TMP_6 t)))) in (let TMP_8 
-\def (next g m) in (let TMP_9 \def (next g TMP_8) in (let TMP_10 \def (TSort 
-TMP_9) in (let TMP_11 \def (next g m) in (let TMP_12 \def (ty3_sort g c0 
-TMP_11) in (ex_intro T TMP_7 TMP_10 TMP_12))))))))) in (let TMP_28 \def 
-(\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda 
-(H0: (getl n c0 (CHead d (Bind Abbr) u))).(\lambda (t: T).(\lambda (_: (ty3 g 
-d u t)).(\lambda (H2: (ex T (\lambda (t0: T).(ty3 g d t t0)))).(let H3 \def 
-H2 in (let TMP_14 \def (\lambda (t0: T).(ty3 g d t t0)) in (let TMP_17 \def 
-(\lambda (t0: T).(let TMP_15 \def (S n) in (let TMP_16 \def (lift TMP_15 O t) 
-in (ty3 g c0 TMP_16 t0)))) in (let TMP_18 \def (ex T TMP_17) in (let TMP_27 
-\def (\lambda (x: T).(\lambda (H4: (ty3 g d t x)).(let TMP_21 \def (\lambda 
-(t0: T).(let TMP_19 \def (S n) in (let TMP_20 \def (lift TMP_19 O t) in (ty3 
-g c0 TMP_20 t0)))) in (let TMP_22 \def (S n) in (let TMP_23 \def (lift TMP_22 
-O x) in (let TMP_24 \def (S n) in (let TMP_25 \def (getl_drop Abbr c0 d u n 
-H0) in (let TMP_26 \def (ty3_lift g d t x H4 c0 O TMP_24 TMP_25) in (ex_intro 
-T TMP_21 TMP_23 TMP_26))))))))) in (ex_ind T TMP_14 TMP_18 TMP_27 
-H3)))))))))))))) in (let TMP_37 \def (\lambda (n: nat).(\lambda (c0: 
+(H: (ty3 g c t1 t2)).(ty3_ind g (\lambda (c0: C).(\lambda (_: T).(\lambda 
+(t0: T).(ex T (\lambda (t3: T).(ty3 g c0 t0 t3)))))) (\lambda (c0: 
+C).(\lambda (t0: T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 t0 t)).(\lambda 
+(_: (ex T (\lambda (t3: T).(ty3 g c0 t t3)))).(\lambda (u: T).(\lambda (t3: 
+T).(\lambda (_: (ty3 g c0 u t3)).(\lambda (_: (ex T (\lambda (t4: T).(ty3 g 
+c0 t3 t4)))).(\lambda (_: (pc3 c0 t3 t0)).(ex_intro T (\lambda (t4: T).(ty3 g 
+c0 t0 t4)) t H0))))))))))) (\lambda (c0: C).(\lambda (m: nat).(ex_intro T 
+(\lambda (t: T).(ty3 g c0 (TSort (next g m)) t)) (TSort (next g (next g m))) 
+(ty3_sort g c0 (next g m))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: 
+C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abbr) 
+u))).(\lambda (t: T).(\lambda (_: (ty3 g d u t)).(\lambda (H2: (ex T (\lambda 
+(t0: T).(ty3 g d t t0)))).(let H3 \def H2 in (ex_ind T (\lambda (t0: T).(ty3 
+g d t t0)) (ex T (\lambda (t0: T).(ty3 g c0 (lift (S n) O t) t0))) (\lambda 
+(x: T).(\lambda (H4: (ty3 g d t x)).(ex_intro T (\lambda (t0: T).(ty3 g c0 
+(lift (S n) O t) t0)) (lift (S n) O x) (ty3_lift g d t x H4 c0 O (S n) 
+(getl_drop Abbr c0 d u n H0))))) H3)))))))))) (\lambda (n: nat).(\lambda (c0: 
 C).(\lambda (d: C).(\lambda (u: T).(\lambda (H0: (getl n c0 (CHead d (Bind 
 Abst) u))).(\lambda (t: T).(\lambda (H1: (ty3 g d u t)).(\lambda (_: (ex T 
-(\lambda (t0: T).(ty3 g d t t0)))).(let TMP_31 \def (\lambda (t0: T).(let 
-TMP_29 \def (S n) in (let TMP_30 \def (lift TMP_29 O u) in (ty3 g c0 TMP_30 
-t0)))) in (let TMP_32 \def (S n) in (let TMP_33 \def (lift TMP_32 O t) in 
-(let TMP_34 \def (S n) in (let TMP_35 \def (getl_drop Abst c0 d u n H0) in 
-(let TMP_36 \def (ty3_lift g d u t H1 c0 O TMP_34 TMP_35) in (ex_intro T 
-TMP_31 TMP_33 TMP_36))))))))))))))) in (let TMP_52 \def (\lambda (c0: 
-C).(\lambda (u: T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u t)).(\lambda (_: 
-(ex T (\lambda (t0: T).(ty3 g c0 t t0)))).(\lambda (b: B).(\lambda (t0: 
-T).(\lambda (t3: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t0 
-t3)).(\lambda (H3: (ex T (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 
-t4)))).(let H4 \def H3 in (let TMP_40 \def (\lambda (t4: T).(let TMP_38 \def 
-(Bind b) in (let TMP_39 \def (CHead c0 TMP_38 u) in (ty3 g TMP_39 t3 t4)))) 
-in (let TMP_43 \def (\lambda (t4: T).(let TMP_41 \def (Bind b) in (let TMP_42 
-\def (THead TMP_41 u t3) in (ty3 g c0 TMP_42 t4)))) in (let TMP_44 \def (ex T 
-TMP_43) in (let TMP_51 \def (\lambda (x: T).(\lambda (H5: (ty3 g (CHead c0 
-(Bind b) u) t3 x)).(let TMP_47 \def (\lambda (t4: T).(let TMP_45 \def (Bind 
-b) in (let TMP_46 \def (THead TMP_45 u t3) in (ty3 g c0 TMP_46 t4)))) in (let 
-TMP_48 \def (Bind b) in (let TMP_49 \def (THead TMP_48 u x) in (let TMP_50 
-\def (ty3_bind g c0 u t H0 b t3 x H5) in (ex_intro T TMP_47 TMP_49 
-TMP_50))))))) in (ex_ind T TMP_40 TMP_44 TMP_51 H4)))))))))))))))) in (let 
-TMP_99 \def (\lambda (c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (H0: 
-(ty3 g c0 w u)).(\lambda (H1: (ex T (\lambda (t: T).(ty3 g c0 u 
-t)))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead (Bind 
-Abst) u t))).(\lambda (H3: (ex T (\lambda (t0: T).(ty3 g c0 (THead (Bind 
-Abst) u t) t0)))).(let H4 \def H1 in (let TMP_53 \def (\lambda (t0: T).(ty3 g 
-c0 u t0)) in (let TMP_58 \def (\lambda (t0: T).(let TMP_54 \def (Flat Appl) 
-in (let TMP_55 \def (Bind Abst) in (let TMP_56 \def (THead TMP_55 u t) in 
-(let TMP_57 \def (THead TMP_54 w TMP_56) in (ty3 g c0 TMP_57 t0)))))) in (let 
-TMP_59 \def (ex T TMP_58) in (let TMP_98 \def (\lambda (x: T).(\lambda (_: 
-(ty3 g c0 u x)).(let H6 \def H3 in (let TMP_62 \def (\lambda (t0: T).(let 
-TMP_60 \def (Bind Abst) in (let TMP_61 \def (THead TMP_60 u t) in (ty3 g c0 
-TMP_61 t0)))) in (let TMP_67 \def (\lambda (t0: T).(let TMP_63 \def (Flat 
-Appl) in (let TMP_64 \def (Bind Abst) in (let TMP_65 \def (THead TMP_64 u t) 
-in (let TMP_66 \def (THead TMP_63 w TMP_65) in (ty3 g c0 TMP_66 t0)))))) in 
-(let TMP_68 \def (ex T TMP_67) in (let TMP_97 \def (\lambda (x0: T).(\lambda 
-(H7: (ty3 g c0 (THead (Bind Abst) u t) x0)).(let TMP_71 \def (\lambda (t3: 
-T).(\lambda (_: T).(let TMP_69 \def (Bind Abst) in (let TMP_70 \def (THead 
-TMP_69 u t3) in (pc3 c0 TMP_70 x0))))) in (let TMP_72 \def (\lambda (_: 
-T).(\lambda (t0: T).(ty3 g c0 u t0))) in (let TMP_75 \def (\lambda (t3: 
-T).(\lambda (_: T).(let TMP_73 \def (Bind Abst) in (let TMP_74 \def (CHead c0 
-TMP_73 u) in (ty3 g TMP_74 t t3))))) in (let TMP_80 \def (\lambda (t0: 
-T).(let TMP_76 \def (Flat Appl) in (let TMP_77 \def (Bind Abst) in (let 
-TMP_78 \def (THead TMP_77 u t) in (let TMP_79 \def (THead TMP_76 w TMP_78) in 
-(ty3 g c0 TMP_79 t0)))))) in (let TMP_81 \def (ex T TMP_80) in (let TMP_95 
-\def (\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c0 (THead (Bind 
-Abst) u x1) x0)).(\lambda (H9: (ty3 g c0 u x2)).(\lambda (H10: (ty3 g (CHead 
-c0 (Bind Abst) u) t x1)).(let TMP_86 \def (\lambda (t0: T).(let TMP_82 \def 
-(Flat Appl) in (let TMP_83 \def (Bind Abst) in (let TMP_84 \def (THead TMP_83 
-u t) in (let TMP_85 \def (THead TMP_82 w TMP_84) in (ty3 g c0 TMP_85 t0)))))) 
-in (let TMP_87 \def (Flat Appl) in (let TMP_88 \def (Bind Abst) in (let 
-TMP_89 \def (THead TMP_88 u x1) in (let TMP_90 \def (THead TMP_87 w TMP_89) 
-in (let TMP_91 \def (Bind Abst) in (let TMP_92 \def (THead TMP_91 u t) in 
-(let TMP_93 \def (ty3_bind g c0 u x2 H9 Abst t x1 H10) in (let TMP_94 \def 
-(ty3_appl g c0 w u H0 TMP_92 x1 TMP_93) in (ex_intro T TMP_86 TMP_90 
-TMP_94))))))))))))))) in (let TMP_96 \def (ty3_gen_bind g Abst c0 u t x0 H7) 
-in (ex3_2_ind T T TMP_71 TMP_72 TMP_75 TMP_81 TMP_95 TMP_96)))))))))) in 
-(ex_ind T TMP_62 TMP_68 TMP_97 H6)))))))) in (ex_ind T TMP_53 TMP_59 TMP_98 
-H4))))))))))))))) in (let TMP_112 \def (\lambda (c0: C).(\lambda (t0: 
-T).(\lambda (t3: T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (_: (ex T 
-(\lambda (t: T).(ty3 g c0 t3 t)))).(\lambda (t4: T).(\lambda (H2: (ty3 g c0 
-t3 t4)).(\lambda (H3: (ex T (\lambda (t: T).(ty3 g c0 t4 t)))).(let H4 \def 
-H3 in (let TMP_100 \def (\lambda (t: T).(ty3 g c0 t4 t)) in (let TMP_103 \def 
-(\lambda (t: T).(let TMP_101 \def (Flat Cast) in (let TMP_102 \def (THead 
-TMP_101 t4 t3) in (ty3 g c0 TMP_102 t)))) in (let TMP_104 \def (ex T TMP_103) 
-in (let TMP_111 \def (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 x)).(let 
-TMP_107 \def (\lambda (t: T).(let TMP_105 \def (Flat Cast) in (let TMP_106 
-\def (THead TMP_105 t4 t3) in (ty3 g c0 TMP_106 t)))) in (let TMP_108 \def 
-(Flat Cast) in (let TMP_109 \def (THead TMP_108 x t4) in (let TMP_110 \def 
-(ty3_cast g c0 t3 t4 H2 x H5) in (ex_intro T TMP_107 TMP_109 TMP_110))))))) 
-in (ex_ind T TMP_100 TMP_104 TMP_111 H4)))))))))))))) in (ty3_ind g TMP_2 
-TMP_4 TMP_13 TMP_28 TMP_37 TMP_52 TMP_99 TMP_112 c t1 t2 H))))))))))))).
+(\lambda (t0: T).(ty3 g d t t0)))).(ex_intro T (\lambda (t0: T).(ty3 g c0 
+(lift (S n) O u) t0)) (lift (S n) O t) (ty3_lift g d u t H1 c0 O (S n) 
+(getl_drop Abst c0 d u n H0))))))))))) (\lambda (c0: C).(\lambda (u: 
+T).(\lambda (t: T).(\lambda (H0: (ty3 g c0 u t)).(\lambda (_: (ex T (\lambda 
+(t0: T).(ty3 g c0 t t0)))).(\lambda (b: B).(\lambda (t0: T).(\lambda (t3: 
+T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u) t0 t3)).(\lambda (H3: (ex T 
+(\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)))).(let H4 \def H3 in 
+(ex_ind T (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t3 t4)) (ex T 
+(\lambda (t4: T).(ty3 g c0 (THead (Bind b) u t3) t4))) (\lambda (x: 
+T).(\lambda (H5: (ty3 g (CHead c0 (Bind b) u) t3 x)).(ex_intro T (\lambda 
+(t4: T).(ty3 g c0 (THead (Bind b) u t3) t4)) (THead (Bind b) u x) (ty3_bind g 
+c0 u t H0 b t3 x H5)))) H4)))))))))))) (\lambda (c0: C).(\lambda (w: 
+T).(\lambda (u: T).(\lambda (H0: (ty3 g c0 w u)).(\lambda (H1: (ex T (\lambda 
+(t: T).(ty3 g c0 u t)))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g 
+c0 v (THead (Bind Abst) u t))).(\lambda (H3: (ex T (\lambda (t0: T).(ty3 g c0 
+(THead (Bind Abst) u t) t0)))).(let H4 \def H1 in (ex_ind T (\lambda (t0: 
+T).(ty3 g c0 u t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w 
+(THead (Bind Abst) u t)) t0))) (\lambda (x: T).(\lambda (_: (ty3 g c0 u 
+x)).(let H6 \def H3 in (ex_ind T (\lambda (t0: T).(ty3 g c0 (THead (Bind 
+Abst) u t) t0)) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w (THead 
+(Bind Abst) u t)) t0))) (\lambda (x0: T).(\lambda (H7: (ty3 g c0 (THead (Bind 
+Abst) u t) x0)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c0 
+(THead (Bind Abst) u t3) x0))) (\lambda (_: T).(\lambda (t0: T).(ty3 g c0 u 
+t0))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c0 (Bind Abst) u) t 
+t3))) (ex T (\lambda (t0: T).(ty3 g c0 (THead (Flat Appl) w (THead (Bind 
+Abst) u t)) t0))) (\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c0 
+(THead (Bind Abst) u x1) x0)).(\lambda (H9: (ty3 g c0 u x2)).(\lambda (H10: 
+(ty3 g (CHead c0 (Bind Abst) u) t x1)).(ex_intro T (\lambda (t0: T).(ty3 g c0 
+(THead (Flat Appl) w (THead (Bind Abst) u t)) t0)) (THead (Flat Appl) w 
+(THead (Bind Abst) u x1)) (ty3_appl g c0 w u H0 (THead (Bind Abst) u t) x1 
+(ty3_bind g c0 u x2 H9 Abst t x1 H10)))))))) (ty3_gen_bind g Abst c0 u t x0 
+H7)))) H6)))) H4))))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t3: 
+T).(\lambda (_: (ty3 g c0 t0 t3)).(\lambda (_: (ex T (\lambda (t: T).(ty3 g 
+c0 t3 t)))).(\lambda (t4: T).(\lambda (H2: (ty3 g c0 t3 t4)).(\lambda (H3: 
+(ex T (\lambda (t: T).(ty3 g c0 t4 t)))).(let H4 \def H3 in (ex_ind T 
+(\lambda (t: T).(ty3 g c0 t4 t)) (ex T (\lambda (t: T).(ty3 g c0 (THead (Flat 
+Cast) t4 t3) t))) (\lambda (x: T).(\lambda (H5: (ty3 g c0 t4 x)).(ex_intro T 
+(\lambda (t: T).(ty3 g c0 (THead (Flat Cast) t4 t3) t)) (THead (Flat Cast) x 
+t4) (ty3_cast g c0 t3 t4 H2 x H5)))) H4)))))))))) c t1 t2 H))))).
 
 theorem ty3_unique:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u 
 t1) \to (\forall (t2: T).((ty3 g c u t2) \to (pc3 c t1 t2)))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (H: 
-(ty3 g c u t1)).(let TMP_1 \def (\lambda (c0: C).(\lambda (t: T).(\lambda 
-(t0: T).(\forall (t2: T).((ty3 g c0 t t2) \to (pc3 c0 t0 t2)))))) in (let 
-TMP_4 \def (\lambda (c0: C).(\lambda (t2: T).(\lambda (t: T).(\lambda (_: 
-(ty3 g c0 t2 t)).(\lambda (_: ((\forall (t3: T).((ty3 g c0 t2 t3) \to (pc3 c0 
-t t3))))).(\lambda (u0: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0 
-t0)).(\lambda (H3: ((\forall (t3: T).((ty3 g c0 u0 t3) \to (pc3 c0 t0 
-t3))))).(\lambda (H4: (pc3 c0 t0 t2)).(\lambda (t3: T).(\lambda (H5: (ty3 g 
-c0 u0 t3)).(let TMP_2 \def (pc3_s c0 t2 t0 H4) in (let TMP_3 \def (H3 t3 H5) 
-in (pc3_t t0 c0 t2 TMP_2 t3 TMP_3))))))))))))))) in (let TMP_5 \def (\lambda 
-(c0: C).(\lambda (m: nat).(\lambda (t2: T).(\lambda (H0: (ty3 g c0 (TSort m) 
-t2)).(ty3_gen_sort g c0 t2 m H0))))) in (let TMP_120 \def (\lambda (n: 
-nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n 
-c0 (CHead d (Bind Abbr) u0))).(\lambda (t: T).(\lambda (_: (ty3 g d u0 
-t)).(\lambda (H2: ((\forall (t2: T).((ty3 g d u0 t2) \to (pc3 d t 
-t2))))).(\lambda (t2: T).(\lambda (H3: (ty3 g c0 (TLRef n) t2)).(let TMP_8 
-\def (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(let TMP_6 \def (S n) 
-in (let TMP_7 \def (lift TMP_6 O t0) in (pc3 c0 TMP_7 t2)))))) in (let TMP_11 
-\def (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(let TMP_9 \def (Bind 
-Abbr) in (let TMP_10 \def (CHead e TMP_9 u1) in (getl n c0 TMP_10)))))) in 
-(let TMP_12 \def (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e 
-u1 t0)))) in (let TMP_13 \def (ex3_3 C T T TMP_8 TMP_11 TMP_12) in (let 
-TMP_16 \def (\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(let TMP_14 \def 
-(S n) in (let TMP_15 \def (lift TMP_14 O u1) in (pc3 c0 TMP_15 t2)))))) in 
-(let TMP_19 \def (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(let TMP_17 
-\def (Bind Abst) in (let TMP_18 \def (CHead e TMP_17 u1) in (getl n c0 
-TMP_18)))))) in (let TMP_20 \def (\lambda (e: C).(\lambda (u1: T).(\lambda 
-(t0: T).(ty3 g e u1 t0)))) in (let TMP_21 \def (ex3_3 C T T TMP_16 TMP_19 
-TMP_20) in (let TMP_22 \def (S n) in (let TMP_23 \def (lift TMP_22 O t) in 
-(let TMP_24 \def (pc3 c0 TMP_23 t2) in (let TMP_83 \def (\lambda (H4: (ex3_3 
-C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O 
-t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead 
-e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 
-g e u1 t0)))))).(let TMP_27 \def (\lambda (_: C).(\lambda (_: T).(\lambda 
-(t0: T).(let TMP_25 \def (S n) in (let TMP_26 \def (lift TMP_25 O t0) in (pc3 
-c0 TMP_26 t2)))))) in (let TMP_30 \def (\lambda (e: C).(\lambda (u1: 
-T).(\lambda (_: T).(let TMP_28 \def (Bind Abbr) in (let TMP_29 \def (CHead e 
-TMP_28 u1) in (getl n c0 TMP_29)))))) in (let TMP_31 \def (\lambda (e: 
-C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))) in (let TMP_32 \def 
-(S n) in (let TMP_33 \def (lift TMP_32 O t) in (let TMP_34 \def (pc3 c0 
-TMP_33 t2) in (let TMP_82 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda 
-(x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O x2) t2)).(\lambda (H6: (getl n c0 
-(CHead x0 (Bind Abbr) x1))).(\lambda (H7: (ty3 g x0 x1 x2)).(let TMP_35 \def 
-(Bind Abbr) in (let TMP_36 \def (CHead d TMP_35 u0) in (let TMP_37 \def 
-(\lambda (c1: C).(getl n c0 c1)) in (let TMP_38 \def (Bind Abbr) in (let 
-TMP_39 \def (CHead x0 TMP_38 x1) in (let TMP_40 \def (Bind Abbr) in (let 
-TMP_41 \def (CHead d TMP_40 u0) in (let TMP_42 \def (Bind Abbr) in (let 
-TMP_43 \def (CHead x0 TMP_42 x1) in (let TMP_44 \def (getl_mono c0 TMP_41 n 
-H0 TMP_43 H6) in (let H8 \def (eq_ind C TMP_36 TMP_37 H0 TMP_39 TMP_44) in 
-(let TMP_45 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow d | 
-(CHead c1 _ _) \Rightarrow c1])) in (let TMP_46 \def (Bind Abbr) in (let 
-TMP_47 \def (CHead d TMP_46 u0) in (let TMP_48 \def (Bind Abbr) in (let 
-TMP_49 \def (CHead x0 TMP_48 x1) in (let TMP_50 \def (Bind Abbr) in (let 
-TMP_51 \def (CHead d TMP_50 u0) in (let TMP_52 \def (Bind Abbr) in (let 
-TMP_53 \def (CHead x0 TMP_52 x1) in (let TMP_54 \def (getl_mono c0 TMP_51 n 
-H0 TMP_53 H6) in (let H9 \def (f_equal C C TMP_45 TMP_47 TMP_49 TMP_54) in 
-(let TMP_55 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow u0 | 
-(CHead _ _ t0) \Rightarrow t0])) in (let TMP_56 \def (Bind Abbr) in (let 
-TMP_57 \def (CHead d TMP_56 u0) in (let TMP_58 \def (Bind Abbr) in (let 
-TMP_59 \def (CHead x0 TMP_58 x1) in (let TMP_60 \def (Bind Abbr) in (let 
-TMP_61 \def (CHead d TMP_60 u0) in (let TMP_62 \def (Bind Abbr) in (let 
-TMP_63 \def (CHead x0 TMP_62 x1) in (let TMP_64 \def (getl_mono c0 TMP_61 n 
-H0 TMP_63 H6) in (let H10 \def (f_equal C T TMP_55 TMP_57 TMP_59 TMP_64) in 
-(let TMP_81 \def (\lambda (H11: (eq C d x0)).(let TMP_67 \def (\lambda (t0: 
-T).(let TMP_65 \def (Bind Abbr) in (let TMP_66 \def (CHead x0 TMP_65 t0) in 
-(getl n c0 TMP_66)))) in (let H12 \def (eq_ind_r T x1 TMP_67 H8 u0 H10) in 
-(let TMP_68 \def (\lambda (t0: T).(ty3 g x0 t0 x2)) in (let H13 \def 
-(eq_ind_r T x1 TMP_68 H7 u0 H10) in (let TMP_71 \def (\lambda (c1: C).(let 
-TMP_69 \def (Bind Abbr) in (let TMP_70 \def (CHead c1 TMP_69 u0) in (getl n 
-c0 TMP_70)))) in (let H14 \def (eq_ind_r C x0 TMP_71 H12 d H11) in (let 
-TMP_72 \def (\lambda (c1: C).(ty3 g c1 u0 x2)) in (let H15 \def (eq_ind_r C 
-x0 TMP_72 H13 d H11) in (let TMP_73 \def (S n) in (let TMP_74 \def (lift 
-TMP_73 O x2) in (let TMP_75 \def (S n) in (let TMP_76 \def (lift TMP_75 O t) 
-in (let TMP_77 \def (S n) in (let TMP_78 \def (getl_drop Abbr c0 d u0 n H14) 
-in (let TMP_79 \def (H2 x2 H15) in (let TMP_80 \def (pc3_lift c0 d TMP_77 O 
-TMP_78 t x2 TMP_79) in (pc3_t TMP_74 c0 TMP_76 TMP_80 t2 H5)))))))))))))))))) 
-in (TMP_81 H9))))))))))))))))))))))))))))))))))))))))) in (ex3_3_ind C T T 
-TMP_27 TMP_30 TMP_31 TMP_34 TMP_82 H4))))))))) in (let TMP_118 \def (\lambda 
-(H4: (ex3_3 C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 
-(lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: 
-T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1: 
-T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(let TMP_86 \def (\lambda (_: 
-C).(\lambda (u1: T).(\lambda (_: T).(let TMP_84 \def (S n) in (let TMP_85 
-\def (lift TMP_84 O u1) in (pc3 c0 TMP_85 t2)))))) in (let TMP_89 \def 
-(\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(let TMP_87 \def (Bind Abst) 
-in (let TMP_88 \def (CHead e TMP_87 u1) in (getl n c0 TMP_88)))))) in (let 
-TMP_90 \def (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 
-t0)))) in (let TMP_91 \def (S n) in (let TMP_92 \def (lift TMP_91 O t) in 
-(let TMP_93 \def (pc3 c0 TMP_92 t2) in (let TMP_117 \def (\lambda (x0: 
-C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c0 (lift (S n) O x1) 
-t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abst) x1))).(\lambda (_: (ty3 g 
-x0 x1 x2)).(let TMP_94 \def (Bind Abbr) in (let TMP_95 \def (CHead d TMP_94 
-u0) in (let TMP_96 \def (\lambda (c1: C).(getl n c0 c1)) in (let TMP_97 \def 
-(Bind Abst) in (let TMP_98 \def (CHead x0 TMP_97 x1) in (let TMP_99 \def 
-(Bind Abbr) in (let TMP_100 \def (CHead d TMP_99 u0) in (let TMP_101 \def 
-(Bind Abst) in (let TMP_102 \def (CHead x0 TMP_101 x1) in (let TMP_103 \def 
-(getl_mono c0 TMP_100 n H0 TMP_102 H6) in (let H8 \def (eq_ind C TMP_95 
-TMP_96 H0 TMP_98 TMP_103) in (let TMP_104 \def (Bind Abbr) in (let TMP_105 
-\def (CHead d TMP_104 u0) in (let TMP_106 \def (\lambda (ee: C).(match ee 
-with [(CSort _) \Rightarrow False | (CHead _ k _) \Rightarrow (match k with 
-[(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True | Abst \Rightarrow 
-False | Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) in (let 
-TMP_107 \def (Bind Abst) in (let TMP_108 \def (CHead x0 TMP_107 x1) in (let 
-TMP_109 \def (Bind Abbr) in (let TMP_110 \def (CHead d TMP_109 u0) in (let 
-TMP_111 \def (Bind Abst) in (let TMP_112 \def (CHead x0 TMP_111 x1) in (let 
-TMP_113 \def (getl_mono c0 TMP_110 n H0 TMP_112 H6) in (let H9 \def (eq_ind C 
-TMP_105 TMP_106 I TMP_108 TMP_113) in (let TMP_114 \def (S n) in (let TMP_115 
-\def (lift TMP_114 O t) in (let TMP_116 \def (pc3 c0 TMP_115 t2) in 
-(False_ind TMP_116 H9)))))))))))))))))))))))))))))))) in (ex3_3_ind C T T 
-TMP_86 TMP_89 TMP_90 TMP_93 TMP_117 H4))))))))) in (let TMP_119 \def 
-(ty3_gen_lref g c0 t2 n H3) in (or_ind TMP_13 TMP_21 TMP_24 TMP_83 TMP_118 
-TMP_119))))))))))))))))))))))))) in (let TMP_230 \def (\lambda (n: 
-nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n 
-c0 (CHead d (Bind Abst) u0))).(\lambda (t: T).(\lambda (_: (ty3 g d u0 
-t)).(\lambda (_: ((\forall (t2: T).((ty3 g d u0 t2) \to (pc3 d t 
-t2))))).(\lambda (t2: T).(\lambda (H3: (ty3 g c0 (TLRef n) t2)).(let TMP_123 
-\def (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(let TMP_121 \def (S n) 
-in (let TMP_122 \def (lift TMP_121 O t0) in (pc3 c0 TMP_122 t2)))))) in (let 
-TMP_126 \def (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(let TMP_124 
-\def (Bind Abbr) in (let TMP_125 \def (CHead e TMP_124 u1) in (getl n c0 
-TMP_125)))))) in (let TMP_127 \def (\lambda (e: C).(\lambda (u1: T).(\lambda 
-(t0: T).(ty3 g e u1 t0)))) in (let TMP_128 \def (ex3_3 C T T TMP_123 TMP_126 
-TMP_127) in (let TMP_131 \def (\lambda (_: C).(\lambda (u1: T).(\lambda (_: 
-T).(let TMP_129 \def (S n) in (let TMP_130 \def (lift TMP_129 O u1) in (pc3 
-c0 TMP_130 t2)))))) in (let TMP_134 \def (\lambda (e: C).(\lambda (u1: 
-T).(\lambda (_: T).(let TMP_132 \def (Bind Abst) in (let TMP_133 \def (CHead 
-e TMP_132 u1) in (getl n c0 TMP_133)))))) in (let TMP_135 \def (\lambda (e: 
-C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))) in (let TMP_136 \def 
-(ex3_3 C T T TMP_131 TMP_134 TMP_135) in (let TMP_137 \def (S n) in (let 
-TMP_138 \def (lift TMP_137 O u0) in (let TMP_139 \def (pc3 c0 TMP_138 t2) in 
-(let TMP_174 \def (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (_: 
+(ty3 g c u t1)).(ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: 
+T).(\forall (t2: T).((ty3 g c0 t t2) \to (pc3 c0 t0 t2)))))) (\lambda (c0: 
+C).(\lambda (t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda 
+(_: ((\forall (t3: T).((ty3 g c0 t2 t3) \to (pc3 c0 t t3))))).(\lambda (u0: 
+T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0 t0)).(\lambda (H3: ((\forall 
+(t3: T).((ty3 g c0 u0 t3) \to (pc3 c0 t0 t3))))).(\lambda (H4: (pc3 c0 t0 
+t2)).(\lambda (t3: T).(\lambda (H5: (ty3 g c0 u0 t3)).(pc3_t t0 c0 t2 (pc3_s 
+c0 t2 t0 H4) t3 (H3 t3 H5)))))))))))))) (\lambda (c0: C).(\lambda (m: 
+nat).(\lambda (t2: T).(\lambda (H0: (ty3 g c0 (TSort m) t2)).(ty3_gen_sort g 
+c0 t2 m H0))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda 
+(u0: T).(\lambda (H0: (getl n c0 (CHead d (Bind Abbr) u0))).(\lambda (t: 
+T).(\lambda (_: (ty3 g d u0 t)).(\lambda (H2: ((\forall (t2: T).((ty3 g d u0 
+t2) \to (pc3 d t t2))))).(\lambda (t2: T).(\lambda (H3: (ty3 g c0 (TLRef n) 
+t2)).(or_ind (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: 
+T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda 
+(_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: 
+T).(\lambda (t0: T).(ty3 g e u1 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda 
+(u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: 
+C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u1))))) 
+(\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0))))) (pc3 c0 
+(lift (S n) O t) t2) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (_: 
 T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda 
 (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: 
-C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(let TMP_142 \def 
-(\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(let TMP_140 \def (S n) in 
-(let TMP_141 \def (lift TMP_140 O t0) in (pc3 c0 TMP_141 t2)))))) in (let 
-TMP_145 \def (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(let TMP_143 
-\def (Bind Abbr) in (let TMP_144 \def (CHead e TMP_143 u1) in (getl n c0 
-TMP_144)))))) in (let TMP_146 \def (\lambda (e: C).(\lambda (u1: T).(\lambda 
-(t0: T).(ty3 g e u1 t0)))) in (let TMP_147 \def (S n) in (let TMP_148 \def 
-(lift TMP_147 O u0) in (let TMP_149 \def (pc3 c0 TMP_148 t2) in (let TMP_173 
-\def (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (_: (pc3 c0 
-(lift (S n) O x2) t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abbr) 
-x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let TMP_150 \def (Bind Abst) in (let 
-TMP_151 \def (CHead d TMP_150 u0) in (let TMP_152 \def (\lambda (c1: C).(getl 
-n c0 c1)) in (let TMP_153 \def (Bind Abbr) in (let TMP_154 \def (CHead x0 
-TMP_153 x1) in (let TMP_155 \def (Bind Abst) in (let TMP_156 \def (CHead d 
-TMP_155 u0) in (let TMP_157 \def (Bind Abbr) in (let TMP_158 \def (CHead x0 
-TMP_157 x1) in (let TMP_159 \def (getl_mono c0 TMP_156 n H0 TMP_158 H6) in 
-(let H8 \def (eq_ind C TMP_151 TMP_152 H0 TMP_154 TMP_159) in (let TMP_160 
-\def (Bind Abst) in (let TMP_161 \def (CHead d TMP_160 u0) in (let TMP_162 
-\def (\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ 
-k _) \Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr 
+C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T 
+(\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) 
+t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e 
+(Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g 
+e u1 t0)))) (pc3 c0 (lift (S n) O t) t2) (\lambda (x0: C).(\lambda (x1: 
+T).(\lambda (x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O x2) t2)).(\lambda 
+(H6: (getl n c0 (CHead x0 (Bind Abbr) x1))).(\lambda (H7: (ty3 g x0 x1 
+x2)).(let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl n 
+c0 c1)) H0 (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n 
+H0 (CHead x0 (Bind Abbr) x1) H6)) in (let H9 \def (f_equal C C (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) 
+(CHead d (Bind Abbr) u0) (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d 
+(Bind Abbr) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in ((let H10 \def 
+(f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow u0 | (CHead 
+_ _ t0) \Rightarrow t0])) (CHead d (Bind Abbr) u0) (CHead x0 (Bind Abbr) x1) 
+(getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in 
+(\lambda (H11: (eq C d x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t0: 
+T).(getl n c0 (CHead x0 (Bind Abbr) t0))) H8 u0 H10) in (let H13 \def 
+(eq_ind_r T x1 (\lambda (t0: T).(ty3 g x0 t0 x2)) H7 u0 H10) in (let H14 \def 
+(eq_ind_r C x0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind Abbr) u0))) H12 d 
+H11) in (let H15 \def (eq_ind_r C x0 (\lambda (c1: C).(ty3 g c1 u0 x2)) H13 d 
+H11) in (pc3_t (lift (S n) O x2) c0 (lift (S n) O t) (pc3_lift c0 d (S n) O 
+(getl_drop Abbr c0 d u0 n H14) t x2 (H2 x2 H15)) t2 H5))))))) H9))))))))) 
+H4)) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_: 
+T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda 
+(_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1: 
+T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T (\lambda (_: 
+C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda 
+(e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) 
+u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))) 
+(pc3 c0 (lift (S n) O t) t2) (\lambda (x0: C).(\lambda (x1: T).(\lambda (x2: 
+T).(\lambda (_: (pc3 c0 (lift (S n) O x1) t2)).(\lambda (H6: (getl n c0 
+(CHead x0 (Bind Abst) x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let H8 \def 
+(eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: C).(getl n c0 c1)) H0 (CHead 
+x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead x0 
+(Bind Abst) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind Abbr) u0) 
+(\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) 
+\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr 
+\Rightarrow True | Abst \Rightarrow False | Void \Rightarrow False]) | (Flat 
+_) \Rightarrow False])])) I (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d 
+(Bind Abbr) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in (False_ind (pc3 c0 
+(lift (S n) O t) t2) H9))))))))) H4)) (ty3_gen_lref g c0 t2 n H3)))))))))))) 
+(\lambda (n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda 
+(H0: (getl n c0 (CHead d (Bind Abst) u0))).(\lambda (t: T).(\lambda (_: (ty3 
+g d u0 t)).(\lambda (_: ((\forall (t2: T).((ty3 g d u0 t2) \to (pc3 d t 
+t2))))).(\lambda (t2: T).(\lambda (H3: (ty3 g c0 (TLRef n) t2)).(or_ind 
+(ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift 
+(S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n 
+c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda 
+(t0: T).(ty3 g e u1 t0))))) (ex3_3 C T T (\lambda (_: C).(\lambda (u1: 
+T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda 
+(u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: 
+C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0))))) (pc3 c0 (lift (S n) 
+O u0) t2) (\lambda (H4: (ex3_3 C T T (\lambda (_: C).(\lambda (_: T).(\lambda 
+(t0: T).(pc3 c0 (lift (S n) O t0) t2)))) (\lambda (e: C).(\lambda (u1: 
+T).(\lambda (_: T).(getl n c0 (CHead e (Bind Abbr) u1))))) (\lambda (e: 
+C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))))).(ex3_3_ind C T T 
+(\lambda (_: C).(\lambda (_: T).(\lambda (t0: T).(pc3 c0 (lift (S n) O t0) 
+t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e 
+(Bind Abbr) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g 
+e u1 t0)))) (pc3 c0 (lift (S n) O u0) t2) (\lambda (x0: C).(\lambda (x1: 
+T).(\lambda (x2: T).(\lambda (_: (pc3 c0 (lift (S n) O x2) t2)).(\lambda (H6: 
+(getl n c0 (CHead x0 (Bind Abbr) x1))).(\lambda (_: (ty3 g x0 x1 x2)).(let H8 
+\def (eq_ind C (CHead d (Bind Abst) u0) (\lambda (c1: C).(getl n c0 c1)) H0 
+(CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead 
+x0 (Bind Abbr) x1) H6)) in (let H9 \def (eq_ind C (CHead d (Bind Abst) u0) 
+(\lambda (ee: C).(match ee with [(CSort _) \Rightarrow False | (CHead _ k _) 
+\Rightarrow (match k with [(Bind b) \Rightarrow (match b with [Abbr 
 \Rightarrow False | Abst \Rightarrow True | Void \Rightarrow False]) | (Flat 
-_) \Rightarrow False])])) in (let TMP_163 \def (Bind Abbr) in (let TMP_164 
-\def (CHead x0 TMP_163 x1) in (let TMP_165 \def (Bind Abst) in (let TMP_166 
-\def (CHead d TMP_165 u0) in (let TMP_167 \def (Bind Abbr) in (let TMP_168 
-\def (CHead x0 TMP_167 x1) in (let TMP_169 \def (getl_mono c0 TMP_166 n H0 
-TMP_168 H6) in (let H9 \def (eq_ind C TMP_161 TMP_162 I TMP_164 TMP_169) in 
-(let TMP_170 \def (S n) in (let TMP_171 \def (lift TMP_170 O u0) in (let 
-TMP_172 \def (pc3 c0 TMP_171 t2) in (False_ind TMP_172 
-H9)))))))))))))))))))))))))))))))) in (ex3_3_ind C T T TMP_142 TMP_145 
-TMP_146 TMP_149 TMP_173 H4))))))))) in (let TMP_228 \def (\lambda (H4: (ex3_3 
-C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O 
-u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead 
-e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 
-g e u1 t0)))))).(let TMP_177 \def (\lambda (_: C).(\lambda (u1: T).(\lambda 
-(_: T).(let TMP_175 \def (S n) in (let TMP_176 \def (lift TMP_175 O u1) in 
-(pc3 c0 TMP_176 t2)))))) in (let TMP_180 \def (\lambda (e: C).(\lambda (u1: 
-T).(\lambda (_: T).(let TMP_178 \def (Bind Abst) in (let TMP_179 \def (CHead 
-e TMP_178 u1) in (getl n c0 TMP_179)))))) in (let TMP_181 \def (\lambda (e: 
-C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 t0)))) in (let TMP_182 \def 
-(S n) in (let TMP_183 \def (lift TMP_182 O u0) in (let TMP_184 \def (pc3 c0 
-TMP_183 t2) in (let TMP_227 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda 
-(x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O x1) t2)).(\lambda (H6: (getl n c0 
-(CHead x0 (Bind Abst) x1))).(\lambda (H7: (ty3 g x0 x1 x2)).(let TMP_185 \def 
-(Bind Abst) in (let TMP_186 \def (CHead d TMP_185 u0) in (let TMP_187 \def 
-(\lambda (c1: C).(getl n c0 c1)) in (let TMP_188 \def (Bind Abst) in (let 
-TMP_189 \def (CHead x0 TMP_188 x1) in (let TMP_190 \def (Bind Abst) in (let 
-TMP_191 \def (CHead d TMP_190 u0) in (let TMP_192 \def (Bind Abst) in (let 
-TMP_193 \def (CHead x0 TMP_192 x1) in (let TMP_194 \def (getl_mono c0 TMP_191 
-n H0 TMP_193 H6) in (let H8 \def (eq_ind C TMP_186 TMP_187 H0 TMP_189 
-TMP_194) in (let TMP_195 \def (\lambda (e: C).(match e with [(CSort _) 
-\Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) in (let TMP_196 \def (Bind 
-Abst) in (let TMP_197 \def (CHead d TMP_196 u0) in (let TMP_198 \def (Bind 
-Abst) in (let TMP_199 \def (CHead x0 TMP_198 x1) in (let TMP_200 \def (Bind 
-Abst) in (let TMP_201 \def (CHead d TMP_200 u0) in (let TMP_202 \def (Bind 
-Abst) in (let TMP_203 \def (CHead x0 TMP_202 x1) in (let TMP_204 \def 
-(getl_mono c0 TMP_201 n H0 TMP_203 H6) in (let H9 \def (f_equal C C TMP_195 
-TMP_197 TMP_199 TMP_204) in (let TMP_205 \def (\lambda (e: C).(match e with 
-[(CSort _) \Rightarrow u0 | (CHead _ _ t0) \Rightarrow t0])) in (let TMP_206 
-\def (Bind Abst) in (let TMP_207 \def (CHead d TMP_206 u0) in (let TMP_208 
-\def (Bind Abst) in (let TMP_209 \def (CHead x0 TMP_208 x1) in (let TMP_210 
-\def (Bind Abst) in (let TMP_211 \def (CHead d TMP_210 u0) in (let TMP_212 
-\def (Bind Abst) in (let TMP_213 \def (CHead x0 TMP_212 x1) in (let TMP_214 
-\def (getl_mono c0 TMP_211 n H0 TMP_213 H6) in (let H10 \def (f_equal C T 
-TMP_205 TMP_207 TMP_209 TMP_214) in (let TMP_226 \def (\lambda (H11: (eq C d 
-x0)).(let TMP_217 \def (\lambda (t0: T).(let TMP_215 \def (Bind Abst) in (let 
-TMP_216 \def (CHead x0 TMP_215 t0) in (getl n c0 TMP_216)))) in (let H12 \def 
-(eq_ind_r T x1 TMP_217 H8 u0 H10) in (let TMP_218 \def (\lambda (t0: T).(ty3 
-g x0 t0 x2)) in (let H13 \def (eq_ind_r T x1 TMP_218 H7 u0 H10) in (let 
-TMP_221 \def (\lambda (t0: T).(let TMP_219 \def (S n) in (let TMP_220 \def 
-(lift TMP_219 O t0) in (pc3 c0 TMP_220 t2)))) in (let H14 \def (eq_ind_r T x1 
-TMP_221 H5 u0 H10) in (let TMP_224 \def (\lambda (c1: C).(let TMP_222 \def 
-(Bind Abst) in (let TMP_223 \def (CHead c1 TMP_222 u0) in (getl n c0 
-TMP_223)))) in (let H15 \def (eq_ind_r C x0 TMP_224 H12 d H11) in (let 
-TMP_225 \def (\lambda (c1: C).(ty3 g c1 u0 x2)) in (let H16 \def (eq_ind_r C 
-x0 TMP_225 H13 d H11) in H14))))))))))) in (TMP_226 
-H9))))))))))))))))))))))))))))))))))))))))) in (ex3_3_ind C T T TMP_177 
-TMP_180 TMP_181 TMP_184 TMP_227 H4))))))))) in (let TMP_229 \def 
-(ty3_gen_lref g c0 t2 n H3) in (or_ind TMP_128 TMP_136 TMP_139 TMP_174 
-TMP_228 TMP_229))))))))))))))))))))))))) in (let TMP_250 \def (\lambda (c0: 
-C).(\lambda (u0: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u0 t)).(\lambda 
-(_: ((\forall (t2: T).((ty3 g c0 u0 t2) \to (pc3 c0 t t2))))).(\lambda (b: 
-B).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) 
-u0) t0 t2)).(\lambda (H3: ((\forall (t3: T).((ty3 g (CHead c0 (Bind b) u0) t0 
-t3) \to (pc3 (CHead c0 (Bind b) u0) t2 t3))))).(\lambda (t3: T).(\lambda (H4: 
-(ty3 g c0 (THead (Bind b) u0 t0) t3)).(let TMP_233 \def (\lambda (t4: 
-T).(\lambda (_: T).(let TMP_231 \def (Bind b) in (let TMP_232 \def (THead 
-TMP_231 u0 t4) in (pc3 c0 TMP_232 t3))))) in (let TMP_234 \def (\lambda (_: 
-T).(\lambda (t5: T).(ty3 g c0 u0 t5))) in (let TMP_237 \def (\lambda (t4: 
-T).(\lambda (_: T).(let TMP_235 \def (Bind b) in (let TMP_236 \def (CHead c0 
-TMP_235 u0) in (ty3 g TMP_236 t0 t4))))) in (let TMP_238 \def (Bind b) in 
-(let TMP_239 \def (THead TMP_238 u0 t2) in (let TMP_240 \def (pc3 c0 TMP_239 
-t3) in (let TMP_248 \def (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 
-c0 (THead (Bind b) u0 x0) t3)).(\lambda (_: (ty3 g c0 u0 x1)).(\lambda (H7: 
-(ty3 g (CHead c0 (Bind b) u0) t0 x0)).(let TMP_241 \def (Bind b) in (let 
-TMP_242 \def (THead TMP_241 u0 x0) in (let TMP_243 \def (Bind b) in (let 
-TMP_244 \def (THead TMP_243 u0 t2) in (let TMP_245 \def (Bind b) in (let 
-TMP_246 \def (H3 x0 H7) in (let TMP_247 \def (pc3_head_2 c0 u0 t2 x0 TMP_245 
-TMP_246) in (pc3_t TMP_242 c0 TMP_244 TMP_247 t3 H5))))))))))))) in (let 
-TMP_249 \def (ty3_gen_bind g b c0 u0 t0 t3 H4) in (ex3_2_ind T T TMP_233 
-TMP_234 TMP_237 TMP_240 TMP_248 TMP_249))))))))))))))))))))) in (let TMP_283 
-\def (\lambda (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 
-w u0)).(\lambda (_: ((\forall (t2: T).((ty3 g c0 w t2) \to (pc3 c0 u0 
-t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 v (THead (Bind 
-Abst) u0 t))).(\lambda (H3: ((\forall (t2: T).((ty3 g c0 v t2) \to (pc3 c0 
-(THead (Bind Abst) u0 t) t2))))).(\lambda (t2: T).(\lambda (H4: (ty3 g c0 
-(THead (Flat Appl) w v) t2)).(let TMP_255 \def (\lambda (u1: T).(\lambda (t0: 
-T).(let TMP_251 \def (Flat Appl) in (let TMP_252 \def (Bind Abst) in (let 
-TMP_253 \def (THead TMP_252 u1 t0) in (let TMP_254 \def (THead TMP_251 w 
-TMP_253) in (pc3 c0 TMP_254 t2))))))) in (let TMP_258 \def (\lambda (u1: 
-T).(\lambda (t0: T).(let TMP_256 \def (Bind Abst) in (let TMP_257 \def (THead 
-TMP_256 u1 t0) in (ty3 g c0 v TMP_257))))) in (let TMP_259 \def (\lambda (u1: 
-T).(\lambda (_: T).(ty3 g c0 w u1))) in (let TMP_260 \def (Flat Appl) in (let 
-TMP_261 \def (Bind Abst) in (let TMP_262 \def (THead TMP_261 u0 t) in (let 
-TMP_263 \def (THead TMP_260 w TMP_262) in (let TMP_264 \def (pc3 c0 TMP_263 
-t2) in (let TMP_281 \def (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 
-c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) t2)).(\lambda (H6: (ty3 g 
-c0 v (THead (Bind Abst) x0 x1))).(\lambda (_: (ty3 g c0 w x0)).(let TMP_265 
-\def (Flat Appl) in (let TMP_266 \def (Bind Abst) in (let TMP_267 \def (THead 
-TMP_266 x0 x1) in (let TMP_268 \def (THead TMP_265 w TMP_267) in (let TMP_269 
-\def (Flat Appl) in (let TMP_270 \def (Bind Abst) in (let TMP_271 \def (THead 
-TMP_270 u0 t) in (let TMP_272 \def (THead TMP_269 w TMP_271) in (let TMP_273 
-\def (Bind Abst) in (let TMP_274 \def (THead TMP_273 u0 t) in (let TMP_275 
-\def (Bind Abst) in (let TMP_276 \def (THead TMP_275 x0 x1) in (let TMP_277 
-\def (Bind Abst) in (let TMP_278 \def (THead TMP_277 x0 x1) in (let TMP_279 
-\def (H3 TMP_278 H6) in (let TMP_280 \def (pc3_thin_dx c0 TMP_274 TMP_276 
-TMP_279 w Appl) in (pc3_t TMP_268 c0 TMP_272 TMP_280 t2 
-H5)))))))))))))))))))))) in (let TMP_282 \def (ty3_gen_appl g c0 w v t2 H4) 
-in (ex3_2_ind T T TMP_255 TMP_258 TMP_259 TMP_264 TMP_281 
-TMP_282)))))))))))))))))))))) in (let TMP_301 \def (\lambda (c0: C).(\lambda 
+_) \Rightarrow False])])) I (CHead x0 (Bind Abbr) x1) (getl_mono c0 (CHead d 
+(Bind Abst) u0) n H0 (CHead x0 (Bind Abbr) x1) H6)) in (False_ind (pc3 c0 
+(lift (S n) O u0) t2) H9))))))))) H4)) (\lambda (H4: (ex3_3 C T T (\lambda 
+(_: C).(\lambda (u1: T).(\lambda (_: T).(pc3 c0 (lift (S n) O u1) t2)))) 
+(\lambda (e: C).(\lambda (u1: T).(\lambda (_: T).(getl n c0 (CHead e (Bind 
+Abst) u1))))) (\lambda (e: C).(\lambda (u1: T).(\lambda (t0: T).(ty3 g e u1 
+t0)))))).(ex3_3_ind C T T (\lambda (_: C).(\lambda (u1: T).(\lambda (_: 
+T).(pc3 c0 (lift (S n) O u1) t2)))) (\lambda (e: C).(\lambda (u1: T).(\lambda 
+(_: T).(getl n c0 (CHead e (Bind Abst) u1))))) (\lambda (e: C).(\lambda (u1: 
+T).(\lambda (t0: T).(ty3 g e u1 t0)))) (pc3 c0 (lift (S n) O u0) t2) (\lambda 
+(x0: C).(\lambda (x1: T).(\lambda (x2: T).(\lambda (H5: (pc3 c0 (lift (S n) O 
+x1) t2)).(\lambda (H6: (getl n c0 (CHead x0 (Bind Abst) x1))).(\lambda (H7: 
+(ty3 g x0 x1 x2)).(let H8 \def (eq_ind C (CHead d (Bind Abst) u0) (\lambda 
+(c1: C).(getl n c0 c1)) H0 (CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d 
+(Bind Abst) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in (let H9 \def (f_equal 
+C C (\lambda (e: C).(match e with [(CSort _) \Rightarrow d | (CHead c1 _ _) 
+\Rightarrow c1])) (CHead d (Bind Abst) u0) (CHead x0 (Bind Abst) x1) 
+(getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead x0 (Bind Abst) x1) H6)) in 
+((let H10 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow u0 | (CHead _ _ t0) \Rightarrow t0])) (CHead d (Bind Abst) u0) 
+(CHead x0 (Bind Abst) x1) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead 
+x0 (Bind Abst) x1) H6)) in (\lambda (H11: (eq C d x0)).(let H12 \def 
+(eq_ind_r T x1 (\lambda (t0: T).(getl n c0 (CHead x0 (Bind Abst) t0))) H8 u0 
+H10) in (let H13 \def (eq_ind_r T x1 (\lambda (t0: T).(ty3 g x0 t0 x2)) H7 u0 
+H10) in (let H14 \def (eq_ind_r T x1 (\lambda (t0: T).(pc3 c0 (lift (S n) O 
+t0) t2)) H5 u0 H10) in (let H15 \def (eq_ind_r C x0 (\lambda (c1: C).(getl n 
+c0 (CHead c1 (Bind Abst) u0))) H12 d H11) in (let H16 \def (eq_ind_r C x0 
+(\lambda (c1: C).(ty3 g c1 u0 x2)) H13 d H11) in H14))))))) H9))))))))) H4)) 
+(ty3_gen_lref g c0 t2 n H3)))))))))))) (\lambda (c0: C).(\lambda (u0: 
+T).(\lambda (t: T).(\lambda (_: (ty3 g c0 u0 t)).(\lambda (_: ((\forall (t2: 
+T).((ty3 g c0 u0 t2) \to (pc3 c0 t t2))))).(\lambda (b: B).(\lambda (t0: 
+T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u0) t0 
+t2)).(\lambda (H3: ((\forall (t3: T).((ty3 g (CHead c0 (Bind b) u0) t0 t3) 
+\to (pc3 (CHead c0 (Bind b) u0) t2 t3))))).(\lambda (t3: T).(\lambda (H4: 
+(ty3 g c0 (THead (Bind b) u0 t0) t3)).(ex3_2_ind T T (\lambda (t4: 
+T).(\lambda (_: T).(pc3 c0 (THead (Bind b) u0 t4) t3))) (\lambda (_: 
+T).(\lambda (t5: T).(ty3 g c0 u0 t5))) (\lambda (t4: T).(\lambda (_: T).(ty3 
+g (CHead c0 (Bind b) u0) t0 t4))) (pc3 c0 (THead (Bind b) u0 t2) t3) (\lambda 
+(x0: T).(\lambda (x1: T).(\lambda (H5: (pc3 c0 (THead (Bind b) u0 x0) 
+t3)).(\lambda (_: (ty3 g c0 u0 x1)).(\lambda (H7: (ty3 g (CHead c0 (Bind b) 
+u0) t0 x0)).(pc3_t (THead (Bind b) u0 x0) c0 (THead (Bind b) u0 t2) 
+(pc3_head_2 c0 u0 t2 x0 (Bind b) (H3 x0 H7)) t3 H5)))))) (ty3_gen_bind g b c0 
+u0 t0 t3 H4)))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u0: 
+T).(\lambda (_: (ty3 g c0 w u0)).(\lambda (_: ((\forall (t2: T).((ty3 g c0 w 
+t2) \to (pc3 c0 u0 t2))))).(\lambda (v: T).(\lambda (t: T).(\lambda (_: (ty3 
+g c0 v (THead (Bind Abst) u0 t))).(\lambda (H3: ((\forall (t2: T).((ty3 g c0 
+v t2) \to (pc3 c0 (THead (Bind Abst) u0 t) t2))))).(\lambda (t2: T).(\lambda 
+(H4: (ty3 g c0 (THead (Flat Appl) w v) t2)).(ex3_2_ind T T (\lambda (u1: 
+T).(\lambda (t0: T).(pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) u1 t0)) 
+t2))) (\lambda (u1: T).(\lambda (t0: T).(ty3 g c0 v (THead (Bind Abst) u1 
+t0)))) (\lambda (u1: T).(\lambda (_: T).(ty3 g c0 w u1))) (pc3 c0 (THead 
+(Flat Appl) w (THead (Bind Abst) u0 t)) t2) (\lambda (x0: T).(\lambda (x1: 
+T).(\lambda (H5: (pc3 c0 (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) 
+t2)).(\lambda (H6: (ty3 g c0 v (THead (Bind Abst) x0 x1))).(\lambda (_: (ty3 
+g c0 w x0)).(pc3_t (THead (Flat Appl) w (THead (Bind Abst) x0 x1)) c0 (THead 
+(Flat Appl) w (THead (Bind Abst) u0 t)) (pc3_thin_dx c0 (THead (Bind Abst) u0 
+t) (THead (Bind Abst) x0 x1) (H3 (THead (Bind Abst) x0 x1) H6) w Appl) t2 
+H5)))))) (ty3_gen_appl g c0 w v t2 H4))))))))))))) (\lambda (c0: C).(\lambda 
 (t0: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (_: 
 ((\forall (t3: T).((ty3 g c0 t0 t3) \to (pc3 c0 t2 t3))))).(\lambda (t3: 
 T).(\lambda (_: (ty3 g c0 t2 t3)).(\lambda (H3: ((\forall (t4: T).((ty3 g c0 
 t2 t4) \to (pc3 c0 t3 t4))))).(\lambda (t4: T).(\lambda (H4: (ty3 g c0 (THead 
-(Flat Cast) t2 t0) t4)).(let TMP_286 \def (\lambda (t5: T).(let TMP_284 \def 
-(Flat Cast) in (let TMP_285 \def (THead TMP_284 t5 t2) in (pc3 c0 TMP_285 
-t4)))) in (let TMP_287 \def (\lambda (_: T).(ty3 g c0 t0 t2)) in (let TMP_288 
-\def (\lambda (t5: T).(ty3 g c0 t2 t5)) in (let TMP_289 \def (Flat Cast) in 
-(let TMP_290 \def (THead TMP_289 t3 t2) in (let TMP_291 \def (pc3 c0 TMP_290 
-t4) in (let TMP_299 \def (\lambda (x0: T).(\lambda (H5: (pc3 c0 (THead (Flat 
-Cast) x0 t2) t4)).(\lambda (_: (ty3 g c0 t0 t2)).(\lambda (H7: (ty3 g c0 t2 
-x0)).(let TMP_292 \def (Flat Cast) in (let TMP_293 \def (THead TMP_292 x0 t2) 
-in (let TMP_294 \def (Flat Cast) in (let TMP_295 \def (THead TMP_294 t3 t2) 
-in (let TMP_296 \def (H3 x0 H7) in (let TMP_297 \def (Flat Cast) in (let 
-TMP_298 \def (pc3_head_1 c0 t3 x0 TMP_296 TMP_297 t2) in (pc3_t TMP_293 c0 
-TMP_295 TMP_298 t4 H5)))))))))))) in (let TMP_300 \def (ty3_gen_cast g c0 t0 
-t2 t4 H4) in (ex3_ind T TMP_286 TMP_287 TMP_288 TMP_291 TMP_299 
-TMP_300))))))))))))))))))) in (ty3_ind g TMP_1 TMP_4 TMP_5 TMP_120 TMP_230 
-TMP_250 TMP_283 TMP_301 c u t1 H))))))))))))).
+(Flat Cast) t2 t0) t4)).(ex3_ind T (\lambda (t5: T).(pc3 c0 (THead (Flat 
+Cast) t5 t2) t4)) (\lambda (_: T).(ty3 g c0 t0 t2)) (\lambda (t5: T).(ty3 g 
+c0 t2 t5)) (pc3 c0 (THead (Flat Cast) t3 t2) t4) (\lambda (x0: T).(\lambda 
+(H5: (pc3 c0 (THead (Flat Cast) x0 t2) t4)).(\lambda (_: (ty3 g c0 t0 
+t2)).(\lambda (H7: (ty3 g c0 t2 x0)).(pc3_t (THead (Flat Cast) x0 t2) c0 
+(THead (Flat Cast) t3 t2) (pc3_head_1 c0 t3 x0 (H3 x0 H7) (Flat Cast) t2) t4 
+H5))))) (ty3_gen_cast g c0 t0 t2 t4 H4)))))))))))) c u t1 H))))).
 
-theorem ty3_gen_abst_abst:
+lemma ty3_gen_abst_abst:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall 
 (t2: T).((ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u t2)) \to (ex2 
 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) 
@@ -833,273 +423,172 @@ u) t1 t2))))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda 
 (t2: T).(\lambda (H: (ty3 g c (THead (Bind Abst) u t1) (THead (Bind Abst) u 
-t2))).(let TMP_3 \def (\lambda (t: T).(let TMP_1 \def (Bind Abst) in (let 
-TMP_2 \def (THead TMP_1 u t2) in (ty3 g c TMP_2 t)))) in (let TMP_4 \def 
-(\lambda (w: T).(ty3 g c u w)) in (let TMP_7 \def (\lambda (_: T).(let TMP_5 
-\def (Bind Abst) in (let TMP_6 \def (CHead c TMP_5 u) in (ty3 g TMP_6 t1 
-t2)))) in (let TMP_8 \def (ex2 T TMP_4 TMP_7) in (let TMP_48 \def (\lambda 
-(x: T).(\lambda (H0: (ty3 g c (THead (Bind Abst) u t2) x)).(let TMP_11 \def 
-(\lambda (t3: T).(\lambda (_: T).(let TMP_9 \def (Bind Abst) in (let TMP_10 
-\def (THead TMP_9 u t3) in (pc3 c TMP_10 x))))) in (let TMP_12 \def (\lambda 
-(_: T).(\lambda (t: T).(ty3 g c u t))) in (let TMP_15 \def (\lambda (t3: 
-T).(\lambda (_: T).(let TMP_13 \def (Bind Abst) in (let TMP_14 \def (CHead c 
-TMP_13 u) in (ty3 g TMP_14 t2 t3))))) in (let TMP_16 \def (\lambda (w: 
-T).(ty3 g c u w)) in (let TMP_19 \def (\lambda (_: T).(let TMP_17 \def (Bind 
-Abst) in (let TMP_18 \def (CHead c TMP_17 u) in (ty3 g TMP_18 t1 t2)))) in 
-(let TMP_20 \def (ex2 T TMP_16 TMP_19) in (let TMP_46 \def (\lambda (x0: 
-T).(\lambda (x1: T).(\lambda (_: (pc3 c (THead (Bind Abst) u x0) x)).(\lambda 
-(_: (ty3 g c u x1)).(\lambda (H3: (ty3 g (CHead c (Bind Abst) u) t2 x0)).(let 
-TMP_25 \def (\lambda (t3: T).(\lambda (_: T).(let TMP_21 \def (Bind Abst) in 
-(let TMP_22 \def (THead TMP_21 u t3) in (let TMP_23 \def (Bind Abst) in (let 
-TMP_24 \def (THead TMP_23 u t2) in (pc3 c TMP_22 TMP_24))))))) in (let TMP_26 
-\def (\lambda (_: T).(\lambda (t: T).(ty3 g c u t))) in (let TMP_29 \def 
-(\lambda (t3: T).(\lambda (_: T).(let TMP_27 \def (Bind Abst) in (let TMP_28 
-\def (CHead c TMP_27 u) in (ty3 g TMP_28 t1 t3))))) in (let TMP_30 \def 
-(\lambda (w: T).(ty3 g c u w)) in (let TMP_33 \def (\lambda (_: T).(let 
-TMP_31 \def (Bind Abst) in (let TMP_32 \def (CHead c TMP_31 u) in (ty3 g 
-TMP_32 t1 t2)))) in (let TMP_34 \def (ex2 T TMP_30 TMP_33) in (let TMP_42 
-\def (\lambda (x2: T).(\lambda (x3: T).(\lambda (H4: (pc3 c (THead (Bind 
-Abst) u x2) (THead (Bind Abst) u t2))).(\lambda (H5: (ty3 g c u x3)).(\lambda 
-(H6: (ty3 g (CHead c (Bind Abst) u) t1 x2)).(let H_y \def (pc3_gen_abst_shift 
-c u x2 t2 H4) in (let TMP_35 \def (\lambda (w: T).(ty3 g c u w)) in (let 
-TMP_38 \def (\lambda (_: T).(let TMP_36 \def (Bind Abst) in (let TMP_37 \def 
-(CHead c TMP_36 u) in (ty3 g TMP_37 t1 t2)))) in (let TMP_39 \def (Bind Abst) 
-in (let TMP_40 \def (CHead c TMP_39 u) in (let TMP_41 \def (ty3_conv g TMP_40 
-t2 x0 H3 t1 x2 H6 H_y) in (ex_intro2 T TMP_35 TMP_38 x3 H5 TMP_41)))))))))))) 
-in (let TMP_43 \def (Bind Abst) in (let TMP_44 \def (THead TMP_43 u t2) in 
-(let TMP_45 \def (ty3_gen_bind g Abst c u t1 TMP_44 H) in (ex3_2_ind T T 
-TMP_25 TMP_26 TMP_29 TMP_34 TMP_42 TMP_45)))))))))))))))) in (let TMP_47 \def 
-(ty3_gen_bind g Abst c u t2 x H0) in (ex3_2_ind T T TMP_11 TMP_12 TMP_15 
-TMP_20 TMP_46 TMP_47))))))))))) in (let TMP_49 \def (Bind Abst) in (let 
-TMP_50 \def (THead TMP_49 u t1) in (let TMP_51 \def (Bind Abst) in (let 
-TMP_52 \def (THead TMP_51 u t2) in (let TMP_53 \def (ty3_correct g c TMP_50 
-TMP_52 H) in (ex_ind T TMP_3 TMP_8 TMP_48 TMP_53)))))))))))))))).
+t2))).(ex_ind T (\lambda (t: T).(ty3 g c (THead (Bind Abst) u t2) t)) (ex2 T 
+(\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) 
+t1 t2))) (\lambda (x: T).(\lambda (H0: (ty3 g c (THead (Bind Abst) u t2) 
+x)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c (THead (Bind Abst) 
+u t3) x))) (\lambda (_: T).(\lambda (t: T).(ty3 g c u t))) (\lambda (t3: 
+T).(\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t2 t3))) (ex2 T (\lambda 
+(w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2))) 
+(\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (pc3 c (THead (Bind Abst) u 
+x0) x)).(\lambda (_: (ty3 g c u x1)).(\lambda (H3: (ty3 g (CHead c (Bind 
+Abst) u) t2 x0)).(ex3_2_ind T T (\lambda (t3: T).(\lambda (_: T).(pc3 c 
+(THead (Bind Abst) u t3) (THead (Bind Abst) u t2)))) (\lambda (_: T).(\lambda 
+(t: T).(ty3 g c u t))) (\lambda (t3: T).(\lambda (_: T).(ty3 g (CHead c (Bind 
+Abst) u) t1 t3))) (ex2 T (\lambda (w: T).(ty3 g c u w)) (\lambda (_: T).(ty3 
+g (CHead c (Bind Abst) u) t1 t2))) (\lambda (x2: T).(\lambda (x3: T).(\lambda 
+(H4: (pc3 c (THead (Bind Abst) u x2) (THead (Bind Abst) u t2))).(\lambda (H5: 
+(ty3 g c u x3)).(\lambda (H6: (ty3 g (CHead c (Bind Abst) u) t1 x2)).(let H_y 
+\def (pc3_gen_abst_shift c u x2 t2 H4) in (ex_intro2 T (\lambda (w: T).(ty3 g 
+c u w)) (\lambda (_: T).(ty3 g (CHead c (Bind Abst) u) t1 t2)) x3 H5 
+(ty3_conv g (CHead c (Bind Abst) u) t2 x0 H3 t1 x2 H6 H_y)))))))) 
+(ty3_gen_bind g Abst c u t1 (THead (Bind Abst) u t2) H))))))) (ty3_gen_bind g 
+Abst c u t2 x H0)))) (ty3_correct g c (THead (Bind Abst) u t1) (THead (Bind 
+Abst) u t2) H))))))).
 
-theorem ty3_typecheck:
+lemma ty3_typecheck:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (v: T).((ty3 g c t 
 v) \to (ex T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (v: T).(\lambda (H: 
-(ty3 g c t v)).(let TMP_1 \def (\lambda (t0: T).(ty3 g c v t0)) in (let TMP_4 
-\def (\lambda (u: T).(let TMP_2 \def (Flat Cast) in (let TMP_3 \def (THead 
-TMP_2 v t) in (ty3 g c TMP_3 u)))) in (let TMP_5 \def (ex T TMP_4) in (let 
-TMP_12 \def (\lambda (x: T).(\lambda (H0: (ty3 g c v x)).(let TMP_8 \def 
-(\lambda (u: T).(let TMP_6 \def (Flat Cast) in (let TMP_7 \def (THead TMP_6 v 
-t) in (ty3 g c TMP_7 u)))) in (let TMP_9 \def (Flat Cast) in (let TMP_10 \def 
-(THead TMP_9 x v) in (let TMP_11 \def (ty3_cast g c t v H x H0) in (ex_intro 
-T TMP_8 TMP_10 TMP_11))))))) in (let TMP_13 \def (ty3_correct g c t v H) in 
-(ex_ind T TMP_1 TMP_5 TMP_12 TMP_13)))))))))).
+(ty3 g c t v)).(ex_ind T (\lambda (t0: T).(ty3 g c v t0)) (ex T (\lambda (u: 
+T).(ty3 g c (THead (Flat Cast) v t) u))) (\lambda (x: T).(\lambda (H0: (ty3 g 
+c v x)).(ex_intro T (\lambda (u: T).(ty3 g c (THead (Flat Cast) v t) u)) 
+(THead (Flat Cast) x v) (ty3_cast g c t v H x H0)))) (ty3_correct g c t v 
+H)))))).
 
-theorem ty3_getl_subst0:
+lemma ty3_getl_subst0:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t 
 u) \to (\forall (v0: T).(\forall (t0: T).(\forall (i: nat).((subst0 i v0 t 
 t0) \to (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c (CHead d 
 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))))
 \def
  \lambda (g: G).(\lambda (c: C).(\lambda (t: T).(\lambda (u: T).(\lambda (H: 
-(ty3 g c t u)).(let TMP_2 \def (\lambda (c0: C).(\lambda (t0: T).(\lambda (_: 
+(ty3 g c t u)).(ty3_ind g (\lambda (c0: C).(\lambda (t0: T).(\lambda (_: 
 T).(\forall (v0: T).(\forall (t2: T).(\forall (i: nat).((subst0 i v0 t0 t2) 
 \to (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d 
-(Bind b) v)) \to (let TMP_1 \def (\lambda (w: T).(ty3 g d v w)) in (ex T 
-TMP_1))))))))))))) in (let TMP_3 \def (\lambda (c0: C).(\lambda (t2: 
-T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (_: ((\forall 
-(v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 t2 t1) \to (\forall 
-(b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b) v)) \to 
-(ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (u0: T).(\lambda 
-(t1: T).(\lambda (_: (ty3 g c0 u0 t1)).(\lambda (H3: ((\forall (v0: 
-T).(\forall (t3: T).(\forall (i: nat).((subst0 i v0 u0 t3) \to (\forall (b: 
-B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b) v)) \to (ex 
-T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (_: (pc3 c0 t1 
-t2)).(\lambda (v0: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H5: 
-(subst0 i v0 u0 t3)).(\lambda (b: B).(\lambda (d: C).(\lambda (v: T).(\lambda 
-(H6: (getl i c0 (CHead d (Bind b) v))).(H3 v0 t3 i H5 b d v 
-H6))))))))))))))))))) in (let TMP_6 \def (\lambda (c0: C).(\lambda (m: 
+(Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))) (\lambda 
+(c0: C).(\lambda (t2: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2 
+t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i: 
+nat).((subst0 i v0 t2 t1) \to (\forall (b: B).(\forall (d: C).(\forall (v: 
+T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v 
+w))))))))))))).(\lambda (u0: T).(\lambda (t1: T).(\lambda (_: (ty3 g c0 u0 
+t1)).(\lambda (H3: ((\forall (v0: T).(\forall (t3: T).(\forall (i: 
+nat).((subst0 i v0 u0 t3) \to (\forall (b: B).(\forall (d: C).(\forall (v: 
+T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v 
+w))))))))))))).(\lambda (_: (pc3 c0 t1 t2)).(\lambda (v0: T).(\lambda (t3: 
+T).(\lambda (i: nat).(\lambda (H5: (subst0 i v0 u0 t3)).(\lambda (b: 
+B).(\lambda (d: C).(\lambda (v: T).(\lambda (H6: (getl i c0 (CHead d (Bind b) 
+v))).(H3 v0 t3 i H5 b d v H6))))))))))))))))))) (\lambda (c0: C).(\lambda (m: 
 nat).(\lambda (v0: T).(\lambda (t0: T).(\lambda (i: nat).(\lambda (H0: 
 (subst0 i v0 (TSort m) t0)).(\lambda (b: B).(\lambda (d: C).(\lambda (v: 
-T).(\lambda (_: (getl i c0 (CHead d (Bind b) v))).(let TMP_4 \def (\lambda 
-(w: T).(ty3 g d v w)) in (let TMP_5 \def (ex T TMP_4) in (subst0_gen_sort v0 
-t0 i m H0 TMP_5))))))))))))) in (let TMP_76 \def (\lambda (n: nat).(\lambda 
+T).(\lambda (_: (getl i c0 (CHead d (Bind b) v))).(subst0_gen_sort v0 t0 i m 
+H0 (ex T (\lambda (w: T).(ty3 g d v w)))))))))))))) (\lambda (n: 
+nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n 
+c0 (CHead d (Bind Abbr) u0))).(\lambda (t0: T).(\lambda (H1: (ty3 g d u0 
+t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i: 
+nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall (d0: C).(\forall (v: 
+T).((getl i d (CHead d0 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d0 v 
+w))))))))))))).(\lambda (v0: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda 
+(H3: (subst0 i v0 (TLRef n) t1)).(\lambda (b: B).(\lambda (d0: C).(\lambda 
+(v: T).(\lambda (H4: (getl i c0 (CHead d0 (Bind b) v))).(land_ind (eq nat n 
+i) (eq T t1 (lift (S n) O v0)) (ex T (\lambda (w: T).(ty3 g d0 v w))) 
+(\lambda (H5: (eq nat n i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let H7 
+\def (eq_ind_r nat i (\lambda (n0: nat).(getl n0 c0 (CHead d0 (Bind b) v))) 
+H4 n H5) in (let H8 \def (eq_ind C (CHead d (Bind Abbr) u0) (\lambda (c1: 
+C).(getl n c0 c1)) H0 (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind 
+Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in (let H9 \def (f_equal C C 
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow d | (CHead c1 _ _) 
+\Rightarrow c1])) (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v) (getl_mono 
+c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in ((let H10 \def 
+(f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow Abbr | 
+(CHead _ k _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) 
+\Rightarrow Abbr])])) (CHead d (Bind Abbr) u0) (CHead d0 (Bind b) v) 
+(getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 (Bind b) v) H7)) in 
+((let H11 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) 
+\Rightarrow u0 | (CHead _ _ t2) \Rightarrow t2])) (CHead d (Bind Abbr) u0) 
+(CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abbr) u0) n H0 (CHead d0 
+(Bind b) v) H7)) in (\lambda (H12: (eq B Abbr b)).(\lambda (H13: (eq C d 
+d0)).(let H14 \def (eq_ind_r T v (\lambda (t2: T).(getl n c0 (CHead d0 (Bind 
+b) t2))) H8 u0 H11) in (eq_ind T u0 (\lambda (t2: T).(ex T (\lambda (w: 
+T).(ty3 g d0 t2 w)))) (let H15 \def (eq_ind_r C d0 (\lambda (c1: C).(getl n 
+c0 (CHead c1 (Bind b) u0))) H14 d H13) in (eq_ind C d (\lambda (c1: C).(ex T 
+(\lambda (w: T).(ty3 g c1 u0 w)))) (let H16 \def (eq_ind_r B b (\lambda (b0: 
+B).(getl n c0 (CHead d (Bind b0) u0))) H15 Abbr H12) in (ex_intro T (\lambda 
+(w: T).(ty3 g d u0 w)) t0 H1)) d0 H13)) v H11))))) H10)) H9)))))) 
+(subst0_gen_lref v0 t1 i n H3)))))))))))))))))) (\lambda (n: nat).(\lambda 
 (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: (getl n c0 (CHead d 
-(Bind Abbr) u0))).(\lambda (t0: T).(\lambda (H1: (ty3 g d u0 t0)).(\lambda 
+(Bind Abst) u0))).(\lambda (t0: T).(\lambda (H1: (ty3 g d u0 t0)).(\lambda 
 (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 u0 t1) 
 \to (\forall (b: B).(\forall (d0: C).(\forall (v: T).((getl i d (CHead d0 
 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d0 v w))))))))))))).(\lambda 
 (v0: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda (H3: (subst0 i v0 (TLRef 
 n) t1)).(\lambda (b: B).(\lambda (d0: C).(\lambda (v: T).(\lambda (H4: (getl 
-i c0 (CHead d0 (Bind b) v))).(let TMP_7 \def (eq nat n i) in (let TMP_8 \def 
-(S n) in (let TMP_9 \def (lift TMP_8 O v0) in (let TMP_10 \def (eq T t1 
-TMP_9) in (let TMP_11 \def (\lambda (w: T).(ty3 g d0 v w)) in (let TMP_12 
-\def (ex T TMP_11) in (let TMP_74 \def (\lambda (H5: (eq nat n i)).(\lambda 
-(_: (eq T t1 (lift (S n) O v0))).(let TMP_15 \def (\lambda (n0: nat).(let 
-TMP_13 \def (Bind b) in (let TMP_14 \def (CHead d0 TMP_13 v) in (getl n0 c0 
-TMP_14)))) in (let H7 \def (eq_ind_r nat i TMP_15 H4 n H5) in (let TMP_16 
-\def (Bind Abbr) in (let TMP_17 \def (CHead d TMP_16 u0) in (let TMP_18 \def 
-(\lambda (c1: C).(getl n c0 c1)) in (let TMP_19 \def (Bind b) in (let TMP_20 
-\def (CHead d0 TMP_19 v) in (let TMP_21 \def (Bind Abbr) in (let TMP_22 \def 
-(CHead d TMP_21 u0) in (let TMP_23 \def (Bind b) in (let TMP_24 \def (CHead 
-d0 TMP_23 v) in (let TMP_25 \def (getl_mono c0 TMP_22 n H0 TMP_24 H7) in (let 
-H8 \def (eq_ind C TMP_17 TMP_18 H0 TMP_20 TMP_25) in (let TMP_26 \def 
-(\lambda (e: C).(match e with [(CSort _) \Rightarrow d | (CHead c1 _ _) 
-\Rightarrow c1])) in (let TMP_27 \def (Bind Abbr) in (let TMP_28 \def (CHead 
-d TMP_27 u0) in (let TMP_29 \def (Bind b) in (let TMP_30 \def (CHead d0 
-TMP_29 v) in (let TMP_31 \def (Bind Abbr) in (let TMP_32 \def (CHead d TMP_31 
-u0) in (let TMP_33 \def (Bind b) in (let TMP_34 \def (CHead d0 TMP_33 v) in 
-(let TMP_35 \def (getl_mono c0 TMP_32 n H0 TMP_34 H7) in (let H9 \def 
-(f_equal C C TMP_26 TMP_28 TMP_30 TMP_35) in (let TMP_36 \def (\lambda (e: 
-C).(match e with [(CSort _) \Rightarrow Abbr | (CHead _ k _) \Rightarrow 
-(match k with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) in 
-(let TMP_37 \def (Bind Abbr) in (let TMP_38 \def (CHead d TMP_37 u0) in (let 
-TMP_39 \def (Bind b) in (let TMP_40 \def (CHead d0 TMP_39 v) in (let TMP_41 
-\def (Bind Abbr) in (let TMP_42 \def (CHead d TMP_41 u0) in (let TMP_43 \def 
-(Bind b) in (let TMP_44 \def (CHead d0 TMP_43 v) in (let TMP_45 \def 
-(getl_mono c0 TMP_42 n H0 TMP_44 H7) in (let H10 \def (f_equal C B TMP_36 
-TMP_38 TMP_40 TMP_45) in (let TMP_46 \def (\lambda (e: C).(match e with 
-[(CSort _) \Rightarrow u0 | (CHead _ _ t2) \Rightarrow t2])) in (let TMP_47 
-\def (Bind Abbr) in (let TMP_48 \def (CHead d TMP_47 u0) in (let TMP_49 \def 
-(Bind b) in (let TMP_50 \def (CHead d0 TMP_49 v) in (let TMP_51 \def (Bind 
-Abbr) in (let TMP_52 \def (CHead d TMP_51 u0) in (let TMP_53 \def (Bind b) in 
-(let TMP_54 \def (CHead d0 TMP_53 v) in (let TMP_55 \def (getl_mono c0 TMP_52 
-n H0 TMP_54 H7) in (let H11 \def (f_equal C T TMP_46 TMP_48 TMP_50 TMP_55) in 
-(let TMP_72 \def (\lambda (H12: (eq B Abbr b)).(\lambda (H13: (eq C d 
-d0)).(let TMP_58 \def (\lambda (t2: T).(let TMP_56 \def (Bind b) in (let 
-TMP_57 \def (CHead d0 TMP_56 t2) in (getl n c0 TMP_57)))) in (let H14 \def 
-(eq_ind_r T v TMP_58 H8 u0 H11) in (let TMP_60 \def (\lambda (t2: T).(let 
-TMP_59 \def (\lambda (w: T).(ty3 g d0 t2 w)) in (ex T TMP_59))) in (let 
-TMP_63 \def (\lambda (c1: C).(let TMP_61 \def (Bind b) in (let TMP_62 \def 
-(CHead c1 TMP_61 u0) in (getl n c0 TMP_62)))) in (let H15 \def (eq_ind_r C d0 
-TMP_63 H14 d H13) in (let TMP_65 \def (\lambda (c1: C).(let TMP_64 \def 
-(\lambda (w: T).(ty3 g c1 u0 w)) in (ex T TMP_64))) in (let TMP_68 \def 
-(\lambda (b0: B).(let TMP_66 \def (Bind b0) in (let TMP_67 \def (CHead d 
-TMP_66 u0) in (getl n c0 TMP_67)))) in (let H16 \def (eq_ind_r B b TMP_68 H15 
-Abbr H12) in (let TMP_69 \def (\lambda (w: T).(ty3 g d u0 w)) in (let TMP_70 
-\def (ex_intro T TMP_69 t0 H1) in (let TMP_71 \def (eq_ind C d TMP_65 TMP_70 
-d0 H13) in (eq_ind T u0 TMP_60 TMP_71 v H11)))))))))))))) in (let TMP_73 \def 
-(TMP_72 H10) in (TMP_73 H9))))))))))))))))))))))))))))))))))))))))))))))))))) 
-in (let TMP_75 \def (subst0_gen_lref v0 t1 i n H3) in (land_ind TMP_7 TMP_10 
-TMP_12 TMP_74 TMP_75))))))))))))))))))))))))) in (let TMP_146 \def (\lambda 
-(n: nat).(\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (H0: 
-(getl n c0 (CHead d (Bind Abst) u0))).(\lambda (t0: T).(\lambda (H1: (ty3 g d 
-u0 t0)).(\lambda (_: ((\forall (v0: T).(\forall (t1: T).(\forall (i: 
-nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall (d0: C).(\forall (v: 
-T).((getl i d (CHead d0 (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d0 v 
-w))))))))))))).(\lambda (v0: T).(\lambda (t1: T).(\lambda (i: nat).(\lambda 
-(H3: (subst0 i v0 (TLRef n) t1)).(\lambda (b: B).(\lambda (d0: C).(\lambda 
-(v: T).(\lambda (H4: (getl i c0 (CHead d0 (Bind b) v))).(let TMP_77 \def (eq 
-nat n i) in (let TMP_78 \def (S n) in (let TMP_79 \def (lift TMP_78 O v0) in 
-(let TMP_80 \def (eq T t1 TMP_79) in (let TMP_81 \def (\lambda (w: T).(ty3 g 
-d0 v w)) in (let TMP_82 \def (ex T TMP_81) in (let TMP_144 \def (\lambda (H5: 
-(eq nat n i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let TMP_85 \def 
-(\lambda (n0: nat).(let TMP_83 \def (Bind b) in (let TMP_84 \def (CHead d0 
-TMP_83 v) in (getl n0 c0 TMP_84)))) in (let H7 \def (eq_ind_r nat i TMP_85 H4 
-n H5) in (let TMP_86 \def (Bind Abst) in (let TMP_87 \def (CHead d TMP_86 u0) 
-in (let TMP_88 \def (\lambda (c1: C).(getl n c0 c1)) in (let TMP_89 \def 
-(Bind b) in (let TMP_90 \def (CHead d0 TMP_89 v) in (let TMP_91 \def (Bind 
-Abst) in (let TMP_92 \def (CHead d TMP_91 u0) in (let TMP_93 \def (Bind b) in 
-(let TMP_94 \def (CHead d0 TMP_93 v) in (let TMP_95 \def (getl_mono c0 TMP_92 
-n H0 TMP_94 H7) in (let H8 \def (eq_ind C TMP_87 TMP_88 H0 TMP_90 TMP_95) in 
-(let TMP_96 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow d | 
-(CHead c1 _ _) \Rightarrow c1])) in (let TMP_97 \def (Bind Abst) in (let 
-TMP_98 \def (CHead d TMP_97 u0) in (let TMP_99 \def (Bind b) in (let TMP_100 
-\def (CHead d0 TMP_99 v) in (let TMP_101 \def (Bind Abst) in (let TMP_102 
-\def (CHead d TMP_101 u0) in (let TMP_103 \def (Bind b) in (let TMP_104 \def 
-(CHead d0 TMP_103 v) in (let TMP_105 \def (getl_mono c0 TMP_102 n H0 TMP_104 
-H7) in (let H9 \def (f_equal C C TMP_96 TMP_98 TMP_100 TMP_105) in (let 
-TMP_106 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow Abst | 
-(CHead _ k _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) 
-\Rightarrow Abst])])) in (let TMP_107 \def (Bind Abst) in (let TMP_108 \def 
-(CHead d TMP_107 u0) in (let TMP_109 \def (Bind b) in (let TMP_110 \def 
-(CHead d0 TMP_109 v) in (let TMP_111 \def (Bind Abst) in (let TMP_112 \def 
-(CHead d TMP_111 u0) in (let TMP_113 \def (Bind b) in (let TMP_114 \def 
-(CHead d0 TMP_113 v) in (let TMP_115 \def (getl_mono c0 TMP_112 n H0 TMP_114 
-H7) in (let H10 \def (f_equal C B TMP_106 TMP_108 TMP_110 TMP_115) in (let 
-TMP_116 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow u0 | (CHead 
-_ _ t2) \Rightarrow t2])) in (let TMP_117 \def (Bind Abst) in (let TMP_118 
-\def (CHead d TMP_117 u0) in (let TMP_119 \def (Bind b) in (let TMP_120 \def 
-(CHead d0 TMP_119 v) in (let TMP_121 \def (Bind Abst) in (let TMP_122 \def 
-(CHead d TMP_121 u0) in (let TMP_123 \def (Bind b) in (let TMP_124 \def 
-(CHead d0 TMP_123 v) in (let TMP_125 \def (getl_mono c0 TMP_122 n H0 TMP_124 
-H7) in (let H11 \def (f_equal C T TMP_116 TMP_118 TMP_120 TMP_125) in (let 
-TMP_142 \def (\lambda (H12: (eq B Abst b)).(\lambda (H13: (eq C d d0)).(let 
-TMP_128 \def (\lambda (t2: T).(let TMP_126 \def (Bind b) in (let TMP_127 \def 
-(CHead d0 TMP_126 t2) in (getl n c0 TMP_127)))) in (let H14 \def (eq_ind_r T 
-v TMP_128 H8 u0 H11) in (let TMP_130 \def (\lambda (t2: T).(let TMP_129 \def 
-(\lambda (w: T).(ty3 g d0 t2 w)) in (ex T TMP_129))) in (let TMP_133 \def 
-(\lambda (c1: C).(let TMP_131 \def (Bind b) in (let TMP_132 \def (CHead c1 
-TMP_131 u0) in (getl n c0 TMP_132)))) in (let H15 \def (eq_ind_r C d0 TMP_133 
-H14 d H13) in (let TMP_135 \def (\lambda (c1: C).(let TMP_134 \def (\lambda 
-(w: T).(ty3 g c1 u0 w)) in (ex T TMP_134))) in (let TMP_138 \def (\lambda 
-(b0: B).(let TMP_136 \def (Bind b0) in (let TMP_137 \def (CHead d TMP_136 u0) 
-in (getl n c0 TMP_137)))) in (let H16 \def (eq_ind_r B b TMP_138 H15 Abst 
-H12) in (let TMP_139 \def (\lambda (w: T).(ty3 g d u0 w)) in (let TMP_140 
-\def (ex_intro T TMP_139 t0 H1) in (let TMP_141 \def (eq_ind C d TMP_135 
-TMP_140 d0 H13) in (eq_ind T u0 TMP_130 TMP_141 v H11)))))))))))))) in (let 
-TMP_143 \def (TMP_142 H10) in (TMP_143 
-H9))))))))))))))))))))))))))))))))))))))))))))))))))) in (let TMP_145 \def 
-(subst0_gen_lref v0 t1 i n H3) in (land_ind TMP_77 TMP_80 TMP_82 TMP_144 
-TMP_145))))))))))))))))))))))))) in (let TMP_205 \def (\lambda (c0: 
-C).(\lambda (u0: T).(\lambda (t0: T).(\lambda (_: (ty3 g c0 u0 t0)).(\lambda 
-(H1: ((\forall (v0: T).(\forall (t1: T).(\forall (i: nat).((subst0 i v0 u0 
-t1) \to (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d 
-(Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (b: 
-B).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) 
-u0) t1 t2)).(\lambda (H3: ((\forall (v0: T).(\forall (t3: T).(\forall (i: 
-nat).((subst0 i v0 t1 t3) \to (\forall (b0: B).(\forall (d: C).(\forall (v: 
-T).((getl i (CHead c0 (Bind b) u0) (CHead d (Bind b0) v)) \to (ex T (\lambda 
-(w: T).(ty3 g d v w))))))))))))).(\lambda (v0: T).(\lambda (t3: T).(\lambda 
-(i: nat).(\lambda (H4: (subst0 i v0 (THead (Bind b) u0 t1) t3)).(\lambda (b0: 
-B).(\lambda (d: C).(\lambda (v: T).(\lambda (H5: (getl i c0 (CHead d (Bind 
-b0) v))).(let TMP_149 \def (\lambda (u2: T).(let TMP_147 \def (Bind b) in 
-(let TMP_148 \def (THead TMP_147 u2 t1) in (eq T t3 TMP_148)))) in (let 
-TMP_150 \def (\lambda (u2: T).(subst0 i v0 u0 u2)) in (let TMP_151 \def (ex2 
-T TMP_149 TMP_150) in (let TMP_154 \def (\lambda (t4: T).(let TMP_152 \def 
-(Bind b) in (let TMP_153 \def (THead TMP_152 u0 t4) in (eq T t3 TMP_153)))) 
-in (let TMP_157 \def (\lambda (t4: T).(let TMP_155 \def (Bind b) in (let 
-TMP_156 \def (s TMP_155 i) in (subst0 TMP_156 v0 t1 t4)))) in (let TMP_158 
-\def (ex2 T TMP_154 TMP_157) in (let TMP_161 \def (\lambda (u2: T).(\lambda 
-(t4: T).(let TMP_159 \def (Bind b) in (let TMP_160 \def (THead TMP_159 u2 t4) 
-in (eq T t3 TMP_160))))) in (let TMP_162 \def (\lambda (u2: T).(\lambda (_: 
-T).(subst0 i v0 u0 u2))) in (let TMP_165 \def (\lambda (_: T).(\lambda (t4: 
-T).(let TMP_163 \def (Bind b) in (let TMP_164 \def (s TMP_163 i) in (subst0 
-TMP_164 v0 t1 t4))))) in (let TMP_166 \def (ex3_2 T T TMP_161 TMP_162 
-TMP_165) in (let TMP_167 \def (\lambda (w: T).(ty3 g d v w)) in (let TMP_168 
-\def (ex T TMP_167) in (let TMP_176 \def (\lambda (H6: (ex2 T (\lambda (u2: 
-T).(eq T t3 (THead (Bind b) u2 t1))) (\lambda (u2: T).(subst0 i v0 u0 
-u2)))).(let TMP_171 \def (\lambda (u2: T).(let TMP_169 \def (Bind b) in (let 
-TMP_170 \def (THead TMP_169 u2 t1) in (eq T t3 TMP_170)))) in (let TMP_172 
-\def (\lambda (u2: T).(subst0 i v0 u0 u2)) in (let TMP_173 \def (\lambda (w: 
-T).(ty3 g d v w)) in (let TMP_174 \def (ex T TMP_173) in (let TMP_175 \def 
-(\lambda (x: T).(\lambda (_: (eq T t3 (THead (Bind b) x t1))).(\lambda (H8: 
-(subst0 i v0 u0 x)).(H1 v0 x i H8 b0 d v H5)))) in (ex2_ind T TMP_171 TMP_172 
-TMP_174 TMP_175 H6))))))) in (let TMP_191 \def (\lambda (H6: (ex2 T (\lambda 
-(t4: T).(eq T t3 (THead (Bind b) u0 t4))) (\lambda (t4: T).(subst0 (s (Bind 
-b) i) v0 t1 t4)))).(let TMP_179 \def (\lambda (t4: T).(let TMP_177 \def (Bind 
-b) in (let TMP_178 \def (THead TMP_177 u0 t4) in (eq T t3 TMP_178)))) in (let 
-TMP_182 \def (\lambda (t4: T).(let TMP_180 \def (Bind b) in (let TMP_181 \def 
-(s TMP_180 i) in (subst0 TMP_181 v0 t1 t4)))) in (let TMP_183 \def (\lambda 
-(w: T).(ty3 g d v w)) in (let TMP_184 \def (ex T TMP_183) in (let TMP_190 
-\def (\lambda (x: T).(\lambda (_: (eq T t3 (THead (Bind b) u0 x))).(\lambda 
-(H8: (subst0 (s (Bind b) i) v0 t1 x)).(let TMP_185 \def (S i) in (let TMP_186 
-\def (Bind b) in (let TMP_187 \def (Bind b0) in (let TMP_188 \def (CHead d 
-TMP_187 v) in (let TMP_189 \def (getl_head TMP_186 i c0 TMP_188 H5 u0) in (H3 
-v0 x TMP_185 H8 b0 d v TMP_189))))))))) in (ex2_ind T TMP_179 TMP_182 TMP_184 
-TMP_190 H6))))))) in (let TMP_202 \def (\lambda (H6: (ex3_2 T T (\lambda (u2: 
-T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2: 
+i c0 (CHead d0 (Bind b) v))).(land_ind (eq nat n i) (eq T t1 (lift (S n) O 
+v0)) (ex T (\lambda (w: T).(ty3 g d0 v w))) (\lambda (H5: (eq nat n 
+i)).(\lambda (_: (eq T t1 (lift (S n) O v0))).(let H7 \def (eq_ind_r nat i 
+(\lambda (n0: nat).(getl n0 c0 (CHead d0 (Bind b) v))) H4 n H5) in (let H8 
+\def (eq_ind C (CHead d (Bind Abst) u0) (\lambda (c1: C).(getl n c0 c1)) H0 
+(CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 (CHead d0 
+(Bind b) v) H7)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e with 
+[(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind 
+Abst) u0) (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind Abst) u0) n H0 
+(CHead d0 (Bind b) v) H7)) in ((let H10 \def (f_equal C B (\lambda (e: 
+C).(match e with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow 
+(match k with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow Abst])])) 
+(CHead d (Bind Abst) u0) (CHead d0 (Bind b) v) (getl_mono c0 (CHead d (Bind 
+Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in ((let H11 \def (f_equal C T 
+(\lambda (e: C).(match e with [(CSort _) \Rightarrow u0 | (CHead _ _ t2) 
+\Rightarrow t2])) (CHead d (Bind Abst) u0) (CHead d0 (Bind b) v) (getl_mono 
+c0 (CHead d (Bind Abst) u0) n H0 (CHead d0 (Bind b) v) H7)) in (\lambda (H12: 
+(eq B Abst b)).(\lambda (H13: (eq C d d0)).(let H14 \def (eq_ind_r T v 
+(\lambda (t2: T).(getl n c0 (CHead d0 (Bind b) t2))) H8 u0 H11) in (eq_ind T 
+u0 (\lambda (t2: T).(ex T (\lambda (w: T).(ty3 g d0 t2 w)))) (let H15 \def 
+(eq_ind_r C d0 (\lambda (c1: C).(getl n c0 (CHead c1 (Bind b) u0))) H14 d 
+H13) in (eq_ind C d (\lambda (c1: C).(ex T (\lambda (w: T).(ty3 g c1 u0 w)))) 
+(let H16 \def (eq_ind_r B b (\lambda (b0: B).(getl n c0 (CHead d (Bind b0) 
+u0))) H15 Abst H12) in (ex_intro T (\lambda (w: T).(ty3 g d u0 w)) t0 H1)) d0 
+H13)) v H11))))) H10)) H9)))))) (subst0_gen_lref v0 t1 i n 
+H3)))))))))))))))))) (\lambda (c0: C).(\lambda (u0: T).(\lambda (t0: 
+T).(\lambda (_: (ty3 g c0 u0 t0)).(\lambda (H1: ((\forall (v0: T).(\forall 
+(t1: T).(\forall (i: nat).((subst0 i v0 u0 t1) \to (\forall (b: B).(\forall 
+(d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda 
+(w: T).(ty3 g d v w))))))))))))).(\lambda (b: B).(\lambda (t1: T).(\lambda 
+(t2: T).(\lambda (_: (ty3 g (CHead c0 (Bind b) u0) t1 t2)).(\lambda (H3: 
+((\forall (v0: T).(\forall (t3: T).(\forall (i: nat).((subst0 i v0 t1 t3) \to 
+(\forall (b0: B).(\forall (d: C).(\forall (v: T).((getl i (CHead c0 (Bind b) 
+u0) (CHead d (Bind b0) v)) \to (ex T (\lambda (w: T).(ty3 g d v 
+w))))))))))))).(\lambda (v0: T).(\lambda (t3: T).(\lambda (i: nat).(\lambda 
+(H4: (subst0 i v0 (THead (Bind b) u0 t1) t3)).(\lambda (b0: B).(\lambda (d: 
+C).(\lambda (v: T).(\lambda (H5: (getl i c0 (CHead d (Bind b0) v))).(or3_ind 
+(ex2 T (\lambda (u2: T).(eq T t3 (THead (Bind b) u2 t1))) (\lambda (u2: 
+T).(subst0 i v0 u0 u2))) (ex2 T (\lambda (t4: T).(eq T t3 (THead (Bind b) u0 
+t4))) (\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4))) (ex3_2 T T (\lambda 
+(u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2: 
 T).(\lambda (_: T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4: 
-T).(subst0 (s (Bind b) i) v0 t1 t4))))).(let TMP_194 \def (\lambda (u2: 
-T).(\lambda (t4: T).(let TMP_192 \def (Bind b) in (let TMP_193 \def (THead 
-TMP_192 u2 t4) in (eq T t3 TMP_193))))) in (let TMP_195 \def (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i v0 u0 u2))) in (let TMP_198 \def (\lambda (_: 
-T).(\lambda (t4: T).(let TMP_196 \def (Bind b) in (let TMP_197 \def (s 
-TMP_196 i) in (subst0 TMP_197 v0 t1 t4))))) in (let TMP_199 \def (\lambda (w: 
-T).(ty3 g d v w)) in (let TMP_200 \def (ex T TMP_199) in (let TMP_201 \def 
-(\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (eq T t3 (THead (Bind b) x0 
-x1))).(\lambda (H8: (subst0 i v0 u0 x0)).(\lambda (_: (subst0 (s (Bind b) i) 
-v0 t1 x1)).(H1 v0 x0 i H8 b0 d v H5)))))) in (ex3_2_ind T T TMP_194 TMP_195 
-TMP_198 TMP_200 TMP_201 H6)))))))) in (let TMP_203 \def (Bind b) in (let 
-TMP_204 \def (subst0_gen_head TMP_203 v0 u0 t1 t3 i H4) in (or3_ind TMP_151 
-TMP_158 TMP_166 TMP_168 TMP_176 TMP_191 TMP_202 
-TMP_204)))))))))))))))))))))))))))))))))))) in (let TMP_263 \def (\lambda 
-(c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 w 
+T).(subst0 (s (Bind b) i) v0 t1 t4)))) (ex T (\lambda (w: T).(ty3 g d v w))) 
+(\lambda (H6: (ex2 T (\lambda (u2: T).(eq T t3 (THead (Bind b) u2 t1))) 
+(\lambda (u2: T).(subst0 i v0 u0 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t3 
+(THead (Bind b) u2 t1))) (\lambda (u2: T).(subst0 i v0 u0 u2)) (ex T (\lambda 
+(w: T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: (eq T t3 (THead (Bind b) 
+x t1))).(\lambda (H8: (subst0 i v0 u0 x)).(H1 v0 x i H8 b0 d v H5)))) H6)) 
+(\lambda (H6: (ex2 T (\lambda (t4: T).(eq T t3 (THead (Bind b) u0 t4))) 
+(\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4)))).(ex2_ind T (\lambda (t4: 
+T).(eq T t3 (THead (Bind b) u0 t4))) (\lambda (t4: T).(subst0 (s (Bind b) i) 
+v0 t1 t4)) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: 
+(eq T t3 (THead (Bind b) u0 x))).(\lambda (H8: (subst0 (s (Bind b) i) v0 t1 
+x)).(H3 v0 x (S i) H8 b0 d v (getl_head (Bind b) i c0 (CHead d (Bind b0) v) 
+H5 u0))))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t4: 
+T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2: T).(\lambda (_: 
+T).(subst0 i v0 u0 u2))) (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Bind b) 
+i) v0 t1 t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 
+(THead (Bind b) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 u0 
+u2))) (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Bind b) i) v0 t1 t4))) (ex 
+T (\lambda (w: T).(ty3 g d v w))) (\lambda (x0: T).(\lambda (x1: T).(\lambda 
+(_: (eq T t3 (THead (Bind b) x0 x1))).(\lambda (H8: (subst0 i v0 u0 
+x0)).(\lambda (_: (subst0 (s (Bind b) i) v0 t1 x1)).(H1 v0 x0 i H8 b0 d v 
+H5)))))) H6)) (subst0_gen_head (Bind b) v0 u0 t1 t3 i H4)))))))))))))))))))) 
+(\lambda (c0: C).(\lambda (w: T).(\lambda (u0: T).(\lambda (_: (ty3 g c0 w 
 u0)).(\lambda (H1: ((\forall (v0: T).(\forall (t0: T).(\forall (i: 
 nat).((subst0 i v0 w t0) \to (\forall (b: B).(\forall (d: C).(\forall (v: 
 T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w0: T).(ty3 g d v 
@@ -1110,116 +599,71 @@ C).(\forall (v1: T).((getl i c0 (CHead d (Bind b) v1)) \to (ex T (\lambda
 (w0: T).(ty3 g d v1 w0))))))))))))).(\lambda (v0: T).(\lambda (t1: 
 T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead (Flat Appl) w v) 
 t1)).(\lambda (b: B).(\lambda (d: C).(\lambda (v1: T).(\lambda (H5: (getl i 
-c0 (CHead d (Bind b) v1))).(let TMP_208 \def (\lambda (u2: T).(let TMP_206 
-\def (Flat Appl) in (let TMP_207 \def (THead TMP_206 u2 v) in (eq T t1 
-TMP_207)))) in (let TMP_209 \def (\lambda (u2: T).(subst0 i v0 w u2)) in (let 
-TMP_210 \def (ex2 T TMP_208 TMP_209) in (let TMP_213 \def (\lambda (t2: 
-T).(let TMP_211 \def (Flat Appl) in (let TMP_212 \def (THead TMP_211 w t2) in 
-(eq T t1 TMP_212)))) in (let TMP_216 \def (\lambda (t2: T).(let TMP_214 \def 
-(Flat Appl) in (let TMP_215 \def (s TMP_214 i) in (subst0 TMP_215 v0 v t2)))) 
-in (let TMP_217 \def (ex2 T TMP_213 TMP_216) in (let TMP_220 \def (\lambda 
-(u2: T).(\lambda (t2: T).(let TMP_218 \def (Flat Appl) in (let TMP_219 \def 
-(THead TMP_218 u2 t2) in (eq T t1 TMP_219))))) in (let TMP_221 \def (\lambda 
-(u2: T).(\lambda (_: T).(subst0 i v0 w u2))) in (let TMP_224 \def (\lambda 
-(_: T).(\lambda (t2: T).(let TMP_222 \def (Flat Appl) in (let TMP_223 \def (s 
-TMP_222 i) in (subst0 TMP_223 v0 v t2))))) in (let TMP_225 \def (ex3_2 T T 
-TMP_220 TMP_221 TMP_224) in (let TMP_226 \def (\lambda (w0: T).(ty3 g d v1 
-w0)) in (let TMP_227 \def (ex T TMP_226) in (let TMP_235 \def (\lambda (H6: 
-(ex2 T (\lambda (u2: T).(eq T t1 (THead (Flat Appl) u2 v))) (\lambda (u2: 
-T).(subst0 i v0 w u2)))).(let TMP_230 \def (\lambda (u2: T).(let TMP_228 \def 
-(Flat Appl) in (let TMP_229 \def (THead TMP_228 u2 v) in (eq T t1 TMP_229)))) 
-in (let TMP_231 \def (\lambda (u2: T).(subst0 i v0 w u2)) in (let TMP_232 
-\def (\lambda (w0: T).(ty3 g d v1 w0)) in (let TMP_233 \def (ex T TMP_232) in 
-(let TMP_234 \def (\lambda (x: T).(\lambda (_: (eq T t1 (THead (Flat Appl) x 
-v))).(\lambda (H8: (subst0 i v0 w x)).(H1 v0 x i H8 b d v1 H5)))) in (ex2_ind 
-T TMP_230 TMP_231 TMP_233 TMP_234 H6))))))) in (let TMP_247 \def (\lambda 
-(H6: (ex2 T (\lambda (t2: T).(eq T t1 (THead (Flat Appl) w t2))) (\lambda 
-(t2: T).(subst0 (s (Flat Appl) i) v0 v t2)))).(let TMP_238 \def (\lambda (t2: 
-T).(let TMP_236 \def (Flat Appl) in (let TMP_237 \def (THead TMP_236 w t2) in 
-(eq T t1 TMP_237)))) in (let TMP_241 \def (\lambda (t2: T).(let TMP_239 \def 
-(Flat Appl) in (let TMP_240 \def (s TMP_239 i) in (subst0 TMP_240 v0 v t2)))) 
-in (let TMP_242 \def (\lambda (w0: T).(ty3 g d v1 w0)) in (let TMP_243 \def 
-(ex T TMP_242) in (let TMP_246 \def (\lambda (x: T).(\lambda (_: (eq T t1 
+c0 (CHead d (Bind b) v1))).(or3_ind (ex2 T (\lambda (u2: T).(eq T t1 (THead 
+(Flat Appl) u2 v))) (\lambda (u2: T).(subst0 i v0 w u2))) (ex2 T (\lambda 
+(t2: T).(eq T t1 (THead (Flat Appl) w t2))) (\lambda (t2: T).(subst0 (s (Flat 
+Appl) i) v0 v t2))) (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t1 
+(THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 w 
+u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2)))) 
+(ex T (\lambda (w0: T).(ty3 g d v1 w0))) (\lambda (H6: (ex2 T (\lambda (u2: 
+T).(eq T t1 (THead (Flat Appl) u2 v))) (\lambda (u2: T).(subst0 i v0 w 
+u2)))).(ex2_ind T (\lambda (u2: T).(eq T t1 (THead (Flat Appl) u2 v))) 
+(\lambda (u2: T).(subst0 i v0 w u2)) (ex T (\lambda (w0: T).(ty3 g d v1 w0))) 
+(\lambda (x: T).(\lambda (_: (eq T t1 (THead (Flat Appl) x v))).(\lambda (H8: 
+(subst0 i v0 w x)).(H1 v0 x i H8 b d v1 H5)))) H6)) (\lambda (H6: (ex2 T 
+(\lambda (t2: T).(eq T t1 (THead (Flat Appl) w t2))) (\lambda (t2: T).(subst0 
+(s (Flat Appl) i) v0 v t2)))).(ex2_ind T (\lambda (t2: T).(eq T t1 (THead 
+(Flat Appl) w t2))) (\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2)) (ex 
+T (\lambda (w0: T).(ty3 g d v1 w0))) (\lambda (x: T).(\lambda (_: (eq T t1 
 (THead (Flat Appl) w x))).(\lambda (H8: (subst0 (s (Flat Appl) i) v0 v 
-x)).(let TMP_244 \def (Flat Appl) in (let TMP_245 \def (s TMP_244 i) in (H3 
-v0 x TMP_245 H8 b d v1 H5)))))) in (ex2_ind T TMP_238 TMP_241 TMP_243 TMP_246 
-H6))))))) in (let TMP_260 \def (\lambda (H6: (ex3_2 T T (\lambda (u2: 
-T).(\lambda (t2: T).(eq T t1 (THead (Flat Appl) u2 t2)))) (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i v0 w u2))) (\lambda (_: T).(\lambda (t2: 
-T).(subst0 (s (Flat Appl) i) v0 v t2))))).(let TMP_250 \def (\lambda (u2: 
-T).(\lambda (t2: T).(let TMP_248 \def (Flat Appl) in (let TMP_249 \def (THead 
-TMP_248 u2 t2) in (eq T t1 TMP_249))))) in (let TMP_251 \def (\lambda (u2: 
-T).(\lambda (_: T).(subst0 i v0 w u2))) in (let TMP_254 \def (\lambda (_: 
-T).(\lambda (t2: T).(let TMP_252 \def (Flat Appl) in (let TMP_253 \def (s 
-TMP_252 i) in (subst0 TMP_253 v0 v t2))))) in (let TMP_255 \def (\lambda (w0: 
-T).(ty3 g d v1 w0)) in (let TMP_256 \def (ex T TMP_255) in (let TMP_259 \def 
-(\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (eq T t1 (THead (Flat Appl) x0 
-x1))).(\lambda (_: (subst0 i v0 w x0)).(\lambda (H9: (subst0 (s (Flat Appl) 
-i) v0 v x1)).(let TMP_257 \def (Flat Appl) in (let TMP_258 \def (s TMP_257 i) 
-in (H3 v0 x1 TMP_258 H9 b d v1 H5)))))))) in (ex3_2_ind T T TMP_250 TMP_251 
-TMP_254 TMP_256 TMP_259 H6)))))))) in (let TMP_261 \def (Flat Appl) in (let 
-TMP_262 \def (subst0_gen_head TMP_261 v0 w v t1 i H4) in (or3_ind TMP_210 
-TMP_217 TMP_225 TMP_227 TMP_235 TMP_247 TMP_260 
-TMP_262))))))))))))))))))))))))))))))))))) in (let TMP_319 \def (\lambda (c0: 
-C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1 t2)).(\lambda 
-(H1: ((\forall (v0: T).(\forall (t0: T).(\forall (i: nat).((subst0 i v0 t1 
-t0) \to (\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d 
-(Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda 
-(t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (H3: ((\forall (v0: 
-T).(\forall (t3: T).(\forall (i: nat).((subst0 i v0 t2 t3) \to (\forall (b: 
-B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b) v)) \to (ex 
-T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (v0: T).(\lambda (t3: 
-T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead (Flat Cast) t2 t1) 
-t3)).(\lambda (b: B).(\lambda (d: C).(\lambda (v: T).(\lambda (H5: (getl i c0 
-(CHead d (Bind b) v))).(let TMP_266 \def (\lambda (u2: T).(let TMP_264 \def 
-(Flat Cast) in (let TMP_265 \def (THead TMP_264 u2 t1) in (eq T t3 
-TMP_265)))) in (let TMP_267 \def (\lambda (u2: T).(subst0 i v0 t2 u2)) in 
-(let TMP_268 \def (ex2 T TMP_266 TMP_267) in (let TMP_271 \def (\lambda (t4: 
-T).(let TMP_269 \def (Flat Cast) in (let TMP_270 \def (THead TMP_269 t2 t4) 
-in (eq T t3 TMP_270)))) in (let TMP_274 \def (\lambda (t4: T).(let TMP_272 
-\def (Flat Cast) in (let TMP_273 \def (s TMP_272 i) in (subst0 TMP_273 v0 t1 
-t4)))) in (let TMP_275 \def (ex2 T TMP_271 TMP_274) in (let TMP_278 \def 
-(\lambda (u2: T).(\lambda (t4: T).(let TMP_276 \def (Flat Cast) in (let 
-TMP_277 \def (THead TMP_276 u2 t4) in (eq T t3 TMP_277))))) in (let TMP_279 
-\def (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 t2 u2))) in (let TMP_282 
-\def (\lambda (_: T).(\lambda (t4: T).(let TMP_280 \def (Flat Cast) in (let 
-TMP_281 \def (s TMP_280 i) in (subst0 TMP_281 v0 t1 t4))))) in (let TMP_283 
-\def (ex3_2 T T TMP_278 TMP_279 TMP_282) in (let TMP_284 \def (\lambda (w: 
-T).(ty3 g d v w)) in (let TMP_285 \def (ex T TMP_284) in (let TMP_293 \def 
-(\lambda (H6: (ex2 T (\lambda (u2: T).(eq T t3 (THead (Flat Cast) u2 t1))) 
-(\lambda (u2: T).(subst0 i v0 t2 u2)))).(let TMP_288 \def (\lambda (u2: 
-T).(let TMP_286 \def (Flat Cast) in (let TMP_287 \def (THead TMP_286 u2 t1) 
-in (eq T t3 TMP_287)))) in (let TMP_289 \def (\lambda (u2: T).(subst0 i v0 t2 
-u2)) in (let TMP_290 \def (\lambda (w: T).(ty3 g d v w)) in (let TMP_291 \def 
-(ex T TMP_290) in (let TMP_292 \def (\lambda (x: T).(\lambda (_: (eq T t3 
-(THead (Flat Cast) x t1))).(\lambda (H8: (subst0 i v0 t2 x)).(H3 v0 x i H8 b 
-d v H5)))) in (ex2_ind T TMP_288 TMP_289 TMP_291 TMP_292 H6))))))) in (let 
-TMP_305 \def (\lambda (H6: (ex2 T (\lambda (t4: T).(eq T t3 (THead (Flat 
-Cast) t2 t4))) (\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 t4)))).(let 
-TMP_296 \def (\lambda (t4: T).(let TMP_294 \def (Flat Cast) in (let TMP_295 
-\def (THead TMP_294 t2 t4) in (eq T t3 TMP_295)))) in (let TMP_299 \def 
-(\lambda (t4: T).(let TMP_297 \def (Flat Cast) in (let TMP_298 \def (s 
-TMP_297 i) in (subst0 TMP_298 v0 t1 t4)))) in (let TMP_300 \def (\lambda (w: 
-T).(ty3 g d v w)) in (let TMP_301 \def (ex T TMP_300) in (let TMP_304 \def 
-(\lambda (x: T).(\lambda (_: (eq T t3 (THead (Flat Cast) t2 x))).(\lambda 
-(H8: (subst0 (s (Flat Cast) i) v0 t1 x)).(let TMP_302 \def (Flat Cast) in 
-(let TMP_303 \def (s TMP_302 i) in (H1 v0 x TMP_303 H8 b d v H5)))))) in 
-(ex2_ind T TMP_296 TMP_299 TMP_301 TMP_304 H6))))))) in (let TMP_316 \def 
+x)).(H3 v0 x (s (Flat Appl) i) H8 b d v1 H5)))) H6)) (\lambda (H6: (ex3_2 T T 
+(\lambda (u2: T).(\lambda (t2: T).(eq T t1 (THead (Flat Appl) u2 t2)))) 
+(\lambda (u2: T).(\lambda (_: T).(subst0 i v0 w u2))) (\lambda (_: 
+T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2))))).(ex3_2_ind T T 
+(\lambda (u2: T).(\lambda (t2: T).(eq T t1 (THead (Flat Appl) u2 t2)))) 
+(\lambda (u2: T).(\lambda (_: T).(subst0 i v0 w u2))) (\lambda (_: 
+T).(\lambda (t2: T).(subst0 (s (Flat Appl) i) v0 v t2))) (ex T (\lambda (w0: 
+T).(ty3 g d v1 w0))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: (eq T t1 
+(THead (Flat Appl) x0 x1))).(\lambda (_: (subst0 i v0 w x0)).(\lambda (H9: 
+(subst0 (s (Flat Appl) i) v0 v x1)).(H3 v0 x1 (s (Flat Appl) i) H9 b d v1 
+H5)))))) H6)) (subst0_gen_head (Flat Appl) v0 w v t1 i H4))))))))))))))))))) 
+(\lambda (c0: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (_: (ty3 g c0 t1 
+t2)).(\lambda (H1: ((\forall (v0: T).(\forall (t0: T).(\forall (i: 
+nat).((subst0 i v0 t1 t0) \to (\forall (b: B).(\forall (d: C).(\forall (v: 
+T).((getl i c0 (CHead d (Bind b) v)) \to (ex T (\lambda (w: T).(ty3 g d v 
+w))))))))))))).(\lambda (t0: T).(\lambda (_: (ty3 g c0 t2 t0)).(\lambda (H3: 
+((\forall (v0: T).(\forall (t3: T).(\forall (i: nat).((subst0 i v0 t2 t3) \to 
+(\forall (b: B).(\forall (d: C).(\forall (v: T).((getl i c0 (CHead d (Bind b) 
+v)) \to (ex T (\lambda (w: T).(ty3 g d v w))))))))))))).(\lambda (v0: 
+T).(\lambda (t3: T).(\lambda (i: nat).(\lambda (H4: (subst0 i v0 (THead (Flat 
+Cast) t2 t1) t3)).(\lambda (b: B).(\lambda (d: C).(\lambda (v: T).(\lambda 
+(H5: (getl i c0 (CHead d (Bind b) v))).(or3_ind (ex2 T (\lambda (u2: T).(eq T 
+t3 (THead (Flat Cast) u2 t1))) (\lambda (u2: T).(subst0 i v0 t2 u2))) (ex2 T 
+(\lambda (t4: T).(eq T t3 (THead (Flat Cast) t2 t4))) (\lambda (t4: 
+T).(subst0 (s (Flat Cast) i) v0 t1 t4))) (ex3_2 T T (\lambda (u2: T).(\lambda 
+(t4: T).(eq T t3 (THead (Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_: 
+T).(subst0 i v0 t2 u2))) (\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat 
+Cast) i) v0 t1 t4)))) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (H6: 
+(ex2 T (\lambda (u2: T).(eq T t3 (THead (Flat Cast) u2 t1))) (\lambda (u2: 
+T).(subst0 i v0 t2 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t3 (THead (Flat 
+Cast) u2 t1))) (\lambda (u2: T).(subst0 i v0 t2 u2)) (ex T (\lambda (w: 
+T).(ty3 g d v w))) (\lambda (x: T).(\lambda (_: (eq T t3 (THead (Flat Cast) x 
+t1))).(\lambda (H8: (subst0 i v0 t2 x)).(H3 v0 x i H8 b d v H5)))) H6)) 
+(\lambda (H6: (ex2 T (\lambda (t4: T).(eq T t3 (THead (Flat Cast) t2 t4))) 
+(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 t4)))).(ex2_ind T (\lambda 
+(t4: T).(eq T t3 (THead (Flat Cast) t2 t4))) (\lambda (t4: T).(subst0 (s 
+(Flat Cast) i) v0 t1 t4)) (ex T (\lambda (w: T).(ty3 g d v w))) (\lambda (x: 
+T).(\lambda (_: (eq T t3 (THead (Flat Cast) t2 x))).(\lambda (H8: (subst0 (s 
+(Flat Cast) i) v0 t1 x)).(H1 v0 x (s (Flat Cast) i) H8 b d v H5)))) H6)) 
 (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead 
 (Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 t2 u2))) 
-(\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 t4))))).(let 
-TMP_308 \def (\lambda (u2: T).(\lambda (t4: T).(let TMP_306 \def (Flat Cast) 
-in (let TMP_307 \def (THead TMP_306 u2 t4) in (eq T t3 TMP_307))))) in (let 
-TMP_309 \def (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 t2 u2))) in (let 
-TMP_312 \def (\lambda (_: T).(\lambda (t4: T).(let TMP_310 \def (Flat Cast) 
-in (let TMP_311 \def (s TMP_310 i) in (subst0 TMP_311 v0 t1 t4))))) in (let 
-TMP_313 \def (\lambda (w: T).(ty3 g d v w)) in (let TMP_314 \def (ex T 
-TMP_313) in (let TMP_315 \def (\lambda (x0: T).(\lambda (x1: T).(\lambda (_: 
-(eq T t3 (THead (Flat Cast) x0 x1))).(\lambda (H8: (subst0 i v0 t2 
+(\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 
+t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead 
+(Flat Cast) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0 t2 u2))) 
+(\lambda (_: T).(\lambda (t4: T).(subst0 (s (Flat Cast) i) v0 t1 t4))) (ex T 
+(\lambda (w: T).(ty3 g d v w))) (\lambda (x0: T).(\lambda (x1: T).(\lambda 
+(_: (eq T t3 (THead (Flat Cast) x0 x1))).(\lambda (H8: (subst0 i v0 t2 
 x0)).(\lambda (_: (subst0 (s (Flat Cast) i) v0 t1 x1)).(H3 v0 x0 i H8 b d v 
-H5)))))) in (ex3_2_ind T T TMP_308 TMP_309 TMP_312 TMP_314 TMP_315 H6)))))))) 
-in (let TMP_317 \def (Flat Cast) in (let TMP_318 \def (subst0_gen_head 
-TMP_317 v0 t2 t1 t3 i H4) in (or3_ind TMP_268 TMP_275 TMP_283 TMP_285 TMP_293 
-TMP_305 TMP_316 TMP_318)))))))))))))))))))))))))))))))))) in (ty3_ind g TMP_2 
-TMP_3 TMP_6 TMP_76 TMP_146 TMP_205 TMP_263 TMP_319 c t u H))))))))))))).
+H5)))))) H6)) (subst0_gen_head (Flat Cast) v0 t2 t1 t3 i H4)))))))))))))))))) 
+c t u H))))).