-C).(csuba g d2 d)))).(let TMP_157 \def (\lambda (d2: C).(let TMP_155 \def
-(Bind Abst) in (let TMP_156 \def (CHead d2 TMP_155 u) in (getl i c2
-TMP_156)))) in (let TMP_158 \def (\lambda (d2: C).(csuba g d2 d)) in (let
-TMP_159 \def (TLRef i) in (let TMP_160 \def (arity g c2 TMP_159 a0) in (let
-TMP_221 \def (\lambda (x: C).(\lambda (H7: (getl i c2 (CHead x (Bind Abst)
-u))).(\lambda (H8: (csuba g x d)).(let H_x0 \def (csubv_getl_conf c2 c H4
-Abst x u i H7) in (let H9 \def H_x0 in (let TMP_161 \def (\lambda (_:
-B).(\lambda (d2: C).(\lambda (_: T).(csubv x d2)))) in (let TMP_164 \def
-(\lambda (b2: B).(\lambda (d2: C).(\lambda (v2: T).(let TMP_162 \def (Bind
-b2) in (let TMP_163 \def (CHead d2 TMP_162 v2) in (getl i c TMP_163)))))) in
-(let TMP_165 \def (TLRef i) in (let TMP_166 \def (arity g c2 TMP_165 a0) in
-(let TMP_220 \def (\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda
-(H10: (csubv x x1)).(\lambda (H11: (getl i c (CHead x1 (Bind x0) x2))).(let
-TMP_167 \def (Bind Abst) in (let TMP_168 \def (CHead d TMP_167 u) in (let
-TMP_169 \def (\lambda (c0: C).(getl i c c0)) in (let TMP_170 \def (Bind x0)
-in (let TMP_171 \def (CHead x1 TMP_170 x2) in (let TMP_172 \def (Bind Abst)
-in (let TMP_173 \def (CHead d TMP_172 u) in (let TMP_174 \def (Bind x0) in
-(let TMP_175 \def (CHead x1 TMP_174 x2) in (let TMP_176 \def (getl_mono c
-TMP_173 i H0 TMP_175 H11) in (let H12 \def (eq_ind C TMP_168 TMP_169 H0
-TMP_171 TMP_176) in (let TMP_177 \def (\lambda (e: C).(match e with [(CSort
-_) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) in (let TMP_178 \def
-(Bind Abst) in (let TMP_179 \def (CHead d TMP_178 u) in (let TMP_180 \def
-(Bind x0) in (let TMP_181 \def (CHead x1 TMP_180 x2) in (let TMP_182 \def
-(Bind Abst) in (let TMP_183 \def (CHead d TMP_182 u) in (let TMP_184 \def
-(Bind x0) in (let TMP_185 \def (CHead x1 TMP_184 x2) in (let TMP_186 \def
-(getl_mono c TMP_183 i H0 TMP_185 H11) in (let H13 \def (f_equal C C TMP_177
-TMP_179 TMP_181 TMP_186) in (let TMP_187 \def (\lambda (e: C).(match e with
-[(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k with [(Bind
-b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) in (let TMP_188 \def (Bind
-Abst) in (let TMP_189 \def (CHead d TMP_188 u) in (let TMP_190 \def (Bind x0)
-in (let TMP_191 \def (CHead x1 TMP_190 x2) in (let TMP_192 \def (Bind Abst)
-in (let TMP_193 \def (CHead d TMP_192 u) in (let TMP_194 \def (Bind x0) in
-(let TMP_195 \def (CHead x1 TMP_194 x2) in (let TMP_196 \def (getl_mono c
-TMP_193 i H0 TMP_195 H11) in (let H14 \def (f_equal C B TMP_187 TMP_189
-TMP_191 TMP_196) in (let TMP_197 \def (\lambda (e: C).(match e with [(CSort
-_) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) in (let TMP_198 \def
-(Bind Abst) in (let TMP_199 \def (CHead d TMP_198 u) in (let TMP_200 \def
-(Bind x0) in (let TMP_201 \def (CHead x1 TMP_200 x2) in (let TMP_202 \def
-(Bind Abst) in (let TMP_203 \def (CHead d TMP_202 u) in (let TMP_204 \def
-(Bind x0) in (let TMP_205 \def (CHead x1 TMP_204 x2) in (let TMP_206 \def
-(getl_mono c TMP_203 i H0 TMP_205 H11) in (let H15 \def (f_equal C T TMP_197
-TMP_199 TMP_201 TMP_206) in (let TMP_218 \def (\lambda (H16: (eq B Abst
-x0)).(\lambda (H17: (eq C d x1)).(let TMP_209 \def (\lambda (t0: T).(let
-TMP_207 \def (Bind x0) in (let TMP_208 \def (CHead x1 TMP_207 t0) in (getl i
-c TMP_208)))) in (let H18 \def (eq_ind_r T x2 TMP_209 H12 u H15) in (let
-TMP_212 \def (\lambda (c0: C).(let TMP_210 \def (Bind x0) in (let TMP_211
-\def (CHead c0 TMP_210 u) in (getl i c TMP_211)))) in (let H19 \def (eq_ind_r
-C x1 TMP_212 H18 d H17) in (let TMP_213 \def (\lambda (c0: C).(csubv x c0))
-in (let H20 \def (eq_ind_r C x1 TMP_213 H10 d H17) in (let TMP_216 \def
-(\lambda (b: B).(let TMP_214 \def (Bind b) in (let TMP_215 \def (CHead d
-TMP_214 u) in (getl i c TMP_215)))) in (let H21 \def (eq_ind_r B x0 TMP_216
-H19 Abst H16) in (let TMP_217 \def (H2 x H8 H20) in (arity_abst g c2 x u i H7
-a0 TMP_217)))))))))))) in (let TMP_219 \def (TMP_218 H14) in (TMP_219
-H13)))))))))))))))))))))))))))))))))))))))))))))))))))) in (ex2_3_ind B C T
-TMP_161 TMP_164 TMP_166 TMP_220 H9))))))))))) in (ex2_ind C TMP_157 TMP_158
-TMP_160 TMP_221 H6))))))) in (let TMP_259 \def (\lambda (H6: (ex2_2 C T
-(\lambda (d2: C).(\lambda (u2: T).(getl i c2 (CHead d2 (Bind Void) u2))))
-(\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))))).(let TMP_225 \def
-(\lambda (d2: C).(\lambda (u2: T).(let TMP_223 \def (Bind Void) in (let
-TMP_224 \def (CHead d2 TMP_223 u2) in (getl i c2 TMP_224))))) in (let TMP_226
-\def (\lambda (d2: C).(\lambda (_: T).(csuba g d2 d))) in (let TMP_227 \def
-(TLRef i) in (let TMP_228 \def (arity g c2 TMP_227 a0) in (let TMP_258 \def
-(\lambda (x0: C).(\lambda (x1: T).(\lambda (H7: (getl i c2 (CHead x0 (Bind
-Void) x1))).(\lambda (_: (csuba g x0 d)).(let H_x0 \def (csubv_getl_conf_void
-c2 c H4 x0 x1 i H7) in (let H9 \def H_x0 in (let TMP_229 \def (\lambda (d2:
-C).(\lambda (_: T).(csubv x0 d2))) in (let TMP_232 \def (\lambda (d2:
-C).(\lambda (v2: T).(let TMP_230 \def (Bind Void) in (let TMP_231 \def (CHead
-d2 TMP_230 v2) in (getl i c TMP_231))))) in (let TMP_233 \def (TLRef i) in
-(let TMP_234 \def (arity g c2 TMP_233 a0) in (let TMP_257 \def (\lambda (x2:
-C).(\lambda (x3: T).(\lambda (_: (csubv x0 x2)).(\lambda (H11: (getl i c
-(CHead x2 (Bind Void) x3))).(let TMP_235 \def (Bind Abst) in (let TMP_236
-\def (CHead d TMP_235 u) in (let TMP_237 \def (\lambda (c0: C).(getl i c c0))
-in (let TMP_238 \def (Bind Void) in (let TMP_239 \def (CHead x2 TMP_238 x3)
-in (let TMP_240 \def (Bind Abst) in (let TMP_241 \def (CHead d TMP_240 u) in
-(let TMP_242 \def (Bind Void) in (let TMP_243 \def (CHead x2 TMP_242 x3) in
-(let TMP_244 \def (getl_mono c TMP_241 i H0 TMP_243 H11) in (let H12 \def
-(eq_ind C TMP_236 TMP_237 H0 TMP_239 TMP_244) in (let TMP_245 \def (Bind
-Abst) in (let TMP_246 \def (CHead d TMP_245 u) in (let TMP_247 \def (\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_248 \def (Bind Void) in (let TMP_249
-\def (CHead x2 TMP_248 x3) in (let TMP_250 \def (Bind Abst) in (let TMP_251
-\def (CHead d TMP_250 u) in (let TMP_252 \def (Bind Void) in (let TMP_253
-\def (CHead x2 TMP_252 x3) in (let TMP_254 \def (getl_mono c TMP_251 i H0
-TMP_253 H11) in (let H13 \def (eq_ind C TMP_246 TMP_247 I TMP_249 TMP_254) in
-(let TMP_255 \def (TLRef i) in (let TMP_256 \def (arity g c2 TMP_255 a0) in
-(False_ind TMP_256 H13))))))))))))))))))))))))))))) in (ex2_2_ind C T TMP_229
-TMP_232 TMP_234 TMP_257 H9)))))))))))) in (ex2_2_ind C T TMP_225 TMP_226
-TMP_228 TMP_258 H6))))))) in (or_ind TMP_147 TMP_152 TMP_154 TMP_222 TMP_259
-H5)))))))))))))))))))))))) in (let TMP_268 \def (\lambda (b: B).(\lambda (H0:
-(not (eq B b Abst))).(\lambda (c: C).(\lambda (u: T).(\lambda (a1:
-A).(\lambda (_: (arity g c u a1)).(\lambda (H2: ((\forall (c2: C).((csuba g
-c2 c) \to ((csubv c2 c) \to (arity g c2 u a1)))))).(\lambda (t0: T).(\lambda
-(a2: A).(\lambda (_: (arity g (CHead c (Bind b) u) t0 a2)).(\lambda (H4:
-((\forall (c2: C).((csuba g c2 (CHead c (Bind b) u)) \to ((csubv c2 (CHead c
-(Bind b) u)) \to (arity g c2 t0 a2)))))).(\lambda (c2: C).(\lambda (H5:
-(csuba g c2 c)).(\lambda (H6: (csubv c2 c)).(let TMP_261 \def (H2 c2 H5 H6)
-in (let TMP_262 \def (Bind b) in (let TMP_263 \def (CHead c2 TMP_262 u) in
-(let TMP_264 \def (Bind b) in (let TMP_265 \def (csuba_head g c2 c H5 TMP_264
-u) in (let TMP_266 \def (csubv_bind_same c2 c H6 b u u) in (let TMP_267 \def
-(H4 TMP_263 TMP_265 TMP_266) in (arity_bind g b H0 c2 u a1 TMP_261 t0 a2
-TMP_267)))))))))))))))))))))) in (let TMP_276 \def (\lambda (c: C).(\lambda
-(u: T).(\lambda (a1: A).(\lambda (_: (arity g c u (asucc g a1))).(\lambda
+C).(csuba g d2 d)))).(ex2_ind C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind
+Abst) u))) (\lambda (d2: C).(csuba g d2 d)) (arity g c2 (TLRef i) a0)
+(\lambda (x: C).(\lambda (H7: (getl i c2 (CHead x (Bind Abst) u))).(\lambda
+(H8: (csuba g x d)).(let H_x0 \def (csubv_getl_conf c2 c H4 Abst x u i H7) in
+(let H9 \def H_x0 in (ex2_3_ind B C T (\lambda (_: B).(\lambda (d2:
+C).(\lambda (_: T).(csubv x d2)))) (\lambda (b2: B).(\lambda (d2: C).(\lambda
+(v2: T).(getl i c (CHead d2 (Bind b2) v2))))) (arity g c2 (TLRef i) a0)
+(\lambda (x0: B).(\lambda (x1: C).(\lambda (x2: T).(\lambda (H10: (csubv x
+x1)).(\lambda (H11: (getl i c (CHead x1 (Bind x0) x2))).(let H12 \def (eq_ind
+C (CHead d (Bind Abst) u) (\lambda (c0: C).(getl i c c0)) H0 (CHead x1 (Bind
+x0) x2) (getl_mono c (CHead d (Bind Abst) u) i H0 (CHead x1 (Bind x0) x2)
+H11)) in (let H13 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abst) u)
+(CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abst) u) i H0 (CHead x1
+(Bind x0) x2) H11)) in ((let H14 \def (f_equal C B (\lambda (e: C).(match e
+with [(CSort _) \Rightarrow Abst | (CHead _ k _) \Rightarrow (match k with
+[(Bind b) \Rightarrow b | (Flat _) \Rightarrow Abst])])) (CHead d (Bind Abst)
+u) (CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abst) u) i H0 (CHead
+x1 (Bind x0) x2) H11)) in ((let H15 \def (f_equal C T (\lambda (e: C).(match
+e with [(CSort _) \Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead d
+(Bind Abst) u) (CHead x1 (Bind x0) x2) (getl_mono c (CHead d (Bind Abst) u) i
+H0 (CHead x1 (Bind x0) x2) H11)) in (\lambda (H16: (eq B Abst x0)).(\lambda
+(H17: (eq C d x1)).(let H18 \def (eq_ind_r T x2 (\lambda (t0: T).(getl i c
+(CHead x1 (Bind x0) t0))) H12 u H15) in (let H19 \def (eq_ind_r C x1 (\lambda
+(c0: C).(getl i c (CHead c0 (Bind x0) u))) H18 d H17) in (let H20 \def
+(eq_ind_r C x1 (\lambda (c0: C).(csubv x c0)) H10 d H17) in (let H21 \def
+(eq_ind_r B x0 (\lambda (b: B).(getl i c (CHead d (Bind b) u))) H19 Abst H16)
+in (arity_abst g c2 x u i H7 a0 (H2 x H8 H20))))))))) H14)) H13))))))))
+H9)))))) H6)) (\lambda (H6: (ex2_2 C T (\lambda (d2: C).(\lambda (u2:
+T).(getl i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_:
+T).(csuba g d2 d))))).(ex2_2_ind C T (\lambda (d2: C).(\lambda (u2: T).(getl
+i c2 (CHead d2 (Bind Void) u2)))) (\lambda (d2: C).(\lambda (_: T).(csuba g
+d2 d))) (arity g c2 (TLRef i) a0) (\lambda (x0: C).(\lambda (x1: T).(\lambda
+(H7: (getl i c2 (CHead x0 (Bind Void) x1))).(\lambda (_: (csuba g x0 d)).(let
+H_x0 \def (csubv_getl_conf_void c2 c H4 x0 x1 i H7) in (let H9 \def H_x0 in
+(ex2_2_ind C T (\lambda (d2: C).(\lambda (_: T).(csubv x0 d2))) (\lambda (d2:
+C).(\lambda (v2: T).(getl i c (CHead d2 (Bind Void) v2)))) (arity g c2 (TLRef
+i) a0) (\lambda (x2: C).(\lambda (x3: T).(\lambda (_: (csubv x0 x2)).(\lambda
+(H11: (getl i c (CHead x2 (Bind Void) x3))).(let H12 \def (eq_ind C (CHead d
+(Bind Abst) u) (\lambda (c0: C).(getl i c c0)) H0 (CHead x2 (Bind Void) x3)
+(getl_mono c (CHead d (Bind Abst) u) i H0 (CHead x2 (Bind Void) x3) H11)) in
+(let H13 \def (eq_ind C (CHead d (Bind Abst) u) (\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])]))
+I (CHead x2 (Bind Void) x3) (getl_mono c (CHead d (Bind Abst) u) i H0 (CHead
+x2 (Bind Void) x3) H11)) in (False_ind (arity g c2 (TLRef i) a0) H13)))))))
+H9))))))) H6)) H5)))))))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b
+Abst))).(\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity
+g c u a1)).(\lambda (H2: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c)
+\to (arity g c2 u a1)))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_:
+(arity g (CHead c (Bind b) u) t0 a2)).(\lambda (H4: ((\forall (c2: C).((csuba
+g c2 (CHead c (Bind b) u)) \to ((csubv c2 (CHead c (Bind b) u)) \to (arity g
+c2 t0 a2)))))).(\lambda (c2: C).(\lambda (H5: (csuba g c2 c)).(\lambda (H6:
+(csubv c2 c)).(arity_bind g b H0 c2 u a1 (H2 c2 H5 H6) t0 a2 (H4 (CHead c2
+(Bind b) u) (csuba_head g c2 c H5 (Bind b) u) (csubv_bind_same c2 c H6 b u
+u))))))))))))))))) (\lambda (c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda
+(_: (arity g c u (asucc g a1))).(\lambda (H1: ((\forall (c2: C).((csuba g c2
+c) \to ((csubv c2 c) \to (arity g c2 u (asucc g a1))))))).(\lambda (t0:
+T).(\lambda (a2: A).(\lambda (_: (arity g (CHead c (Bind Abst) u) t0
+a2)).(\lambda (H3: ((\forall (c2: C).((csuba g c2 (CHead c (Bind Abst) u))
+\to ((csubv c2 (CHead c (Bind Abst) u)) \to (arity g c2 t0 a2)))))).(\lambda
+(c2: C).(\lambda (H4: (csuba g c2 c)).(\lambda (H5: (csubv c2 c)).(arity_head
+g c2 u a1 (H1 c2 H4 H5) t0 a2 (H3 (CHead c2 (Bind Abst) u) (csuba_head g c2 c
+H4 (Bind Abst) u) (csubv_bind_same c2 c H5 Abst u u))))))))))))))) (\lambda
+(c: C).(\lambda (u: T).(\lambda (a1: A).(\lambda (_: (arity g c u
+a1)).(\lambda (H1: ((\forall (c2: C).((csuba g c2 c) \to ((csubv c2 c) \to
+(arity g c2 u a1)))))).(\lambda (t0: T).(\lambda (a2: A).(\lambda (_: (arity
+g c t0 (AHead a1 a2))).(\lambda (H3: ((\forall (c2: C).((csuba g c2 c) \to
+((csubv c2 c) \to (arity g c2 t0 (AHead a1 a2))))))).(\lambda (c2:
+C).(\lambda (H4: (csuba g c2 c)).(\lambda (H5: (csubv c2 c)).(arity_appl g c2
+u a1 (H1 c2 H4 H5) t0 a2 (H3 c2 H4 H5)))))))))))))) (\lambda (c: C).(\lambda
+(u: T).(\lambda (a0: A).(\lambda (_: (arity g c u (asucc g a0))).(\lambda