-x (CHead d1 (Bind Abst) u1))).((match x in C return (\lambda (c: C).((drop i
-O c1 c) \to ((clear c (CHead d1 (Bind Abst) u1)) \to (\forall (c2: C).((csuba
-g c1 c2) \to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst)
-u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
-C).(\lambda (u2: T).(\lambda (_: A).(getl i c2 (CHead d2 (Bind Abbr) u2)))))
-(\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda
-(_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g a)))))
-(\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2 a)))))))))))
-with [(CSort n) \Rightarrow (\lambda (_: (drop i O c1 (CSort n))).(\lambda
-(H4: (clear (CSort n) (CHead d1 (Bind Abst) u1))).(clear_gen_sort (CHead d1
-(Bind Abst) u1) n H4 (\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C
-(\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2:
-C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda
-(_: A).(getl i c2 (CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_:
-T).(\lambda (_: A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_:
-T).(\lambda (a: A).(arity g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda
-(u2: T).(\lambda (a: A).(arity g d2 u2 a))))))))))) | (CHead c k t)
-\Rightarrow (\lambda (H3: (drop i O c1 (CHead c k t))).(\lambda (H4: (clear
-(CHead c k t) (CHead d1 (Bind Abst) u1))).((match k in K return (\lambda (k0:
-K).((drop i O c1 (CHead c k0 t)) \to ((clear (CHead c k0 t) (CHead d1 (Bind
-Abst) u1)) \to (\forall (c2: C).((csuba g c1 c2) \to (or (ex2 C (\lambda (d2:
-C).(getl i c2 (CHead d2 (Bind Abst) u1))) (\lambda (d2: C).(csuba g d1 d2)))
-(ex4_3 C T A (\lambda (d2: C).(\lambda (u2: T).(\lambda (_: A).(getl i c2
-(CHead d2 (Bind Abbr) u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_:
-A).(csuba g d1 d2)))) (\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity
-g d1 u1 (asucc g a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a:
-A).(arity g d2 u2 a))))))))))) with [(Bind b) \Rightarrow (\lambda (H5: (drop
-i O c1 (CHead c (Bind b) t))).(\lambda (H6: (clear (CHead c (Bind b) t)
-(CHead d1 (Bind Abst) u1))).(let H7 \def (f_equal C C (\lambda (e: C).(match
-e in C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d1 | (CHead c0 _
-_) \Rightarrow c0])) (CHead d1 (Bind Abst) u1) (CHead c (Bind b) t)
-(clear_gen_bind b c (CHead d1 (Bind Abst) u1) t H6)) in ((let H8 \def
-(f_equal C B (\lambda (e: C).(match e in C return (\lambda (_: C).B) with
-[(CSort _) \Rightarrow Abst | (CHead _ k0 _) \Rightarrow (match k0 in K
-return (\lambda (_: K).B) with [(Bind b0) \Rightarrow b0 | (Flat _)
-\Rightarrow Abst])])) (CHead d1 (Bind Abst) u1) (CHead c (Bind b) t)
-(clear_gen_bind b c (CHead d1 (Bind Abst) u1) t H6)) in ((let H9 \def
-(f_equal C T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with
-[(CSort _) \Rightarrow u1 | (CHead _ _ t0) \Rightarrow t0])) (CHead d1 (Bind
-Abst) u1) (CHead c (Bind b) t) (clear_gen_bind b c (CHead d1 (Bind Abst) u1)
-t H6)) in (\lambda (H10: (eq B Abst b)).(\lambda (H11: (eq C d1 c)).(\lambda
-(c2: C).(\lambda (H12: (csuba g c1 c2)).(let H13 \def (eq_ind_r T t (\lambda
-(t0: T).(drop i O c1 (CHead c (Bind b) t0))) H5 u1 H9) in (let H14 \def
-(eq_ind_r B b (\lambda (b0: B).(drop i O c1 (CHead c (Bind b0) u1))) H13 Abst
-H10) in (let H15 \def (eq_ind_r C c (\lambda (c0: C).(drop i O c1 (CHead c0
-(Bind Abst) u1))) H14 d1 H11) in (let H16 \def (csuba_drop_abst i c1 d1 u1
-H15 g c2 H12) in (or_ind (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind
-Abst) u1))) (\lambda (d2: C).(csuba g d1 d2))) (ex4_3 C T A (\lambda (d2:
-C).(\lambda (u2: T).(\lambda (_: A).(drop i O c2 (CHead d2 (Bind Abbr)
-u2))))) (\lambda (d2: C).(\lambda (_: T).(\lambda (_: A).(csuba g d1 d2))))
-(\lambda (_: C).(\lambda (_: T).(\lambda (a: A).(arity g d1 u1 (asucc g
-a))))) (\lambda (d2: C).(\lambda (u2: T).(\lambda (a: A).(arity g d2 u2
-a))))) (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u1)))