- \lambda (x2: C).(C_ind (\lambda (c: C).(\forall (x1: C).(\forall (h:
-nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2:
-C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1:
-C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
-c2)))))))))))) (\lambda (n: nat).(\lambda (x1: C).(\lambda (h: nat).(\lambda
-(d: nat).(\lambda (_: (drop h (S d) x1 (CSort n))).(\lambda (b: B).(\lambda
-(c2: C).(\lambda (u: T).(\lambda (H0: (clear (CSort n) (CHead c2 (Bind b)
-u))).(clear_gen_sort (CHead c2 (Bind b) u) n H0 (ex2 C (\lambda (c1:
-C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
-c2))))))))))))) (\lambda (c: C).(\lambda (H: ((\forall (x1: C).(\forall (h:
-nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall (c2:
-C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (ex2 C (\lambda (c1:
-C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1
-c2))))))))))))).(\lambda (k: K).(\lambda (t: T).(\lambda (x1: C).(\lambda (h:
-nat).(\lambda (d: nat).(\lambda (H0: (drop h (S d) x1 (CHead c k
-t))).(\lambda (b: B).(\lambda (c2: C).(\lambda (u: T).(\lambda (H1: (clear
-(CHead c k t) (CHead c2 (Bind b) u))).(ex2_ind C (\lambda (e: C).(eq C x1
-(CHead e k (lift h (r k d) t)))) (\lambda (e: C).(drop h (r k d) e c)) (ex2 C
-(\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1:
-C).(drop h d c1 c2))) (\lambda (x: C).(\lambda (H2: (eq C x1 (CHead x k (lift
-h (r k d) t)))).(\lambda (H3: (drop h (r k d) x c)).(eq_ind_r C (CHead x k
-(lift h (r k d) t)) (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear c0 (CHead
-c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2)))) (K_ind
-(\lambda (k0: K).((clear (CHead c k0 t) (CHead c2 (Bind b) u)) \to ((drop h
-(r k0 d) x c) \to (ex2 C (\lambda (c1: C).(clear (CHead x k0 (lift h (r k0 d)
-t)) (CHead c1 (Bind b) (lift h d u)))) (\lambda (c1: C).(drop h d c1 c2))))))
-(\lambda (b0: B).(\lambda (H4: (clear (CHead c (Bind b0) t) (CHead c2 (Bind
-b) u))).(\lambda (H5: (drop h (r (Bind b0) d) x c)).(let H6 \def (f_equal C C
-(\lambda (e: C).(match e in C return (\lambda (_: C).C) with [(CSort _)
-\Rightarrow c2 | (CHead c0 _ _) \Rightarrow c0])) (CHead c2 (Bind b) u)
-(CHead c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in
-((let H7 \def (f_equal C B (\lambda (e: C).(match e in C return (\lambda (_:
-C).B) with [(CSort _) \Rightarrow b | (CHead _ k0 _) \Rightarrow (match k0 in
-K return (\lambda (_: K).B) with [(Bind b1) \Rightarrow b1 | (Flat _)
-\Rightarrow b])])) (CHead c2 (Bind b) u) (CHead c (Bind b0) t)
-(clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in ((let H8 \def (f_equal C
-T (\lambda (e: C).(match e in C return (\lambda (_: C).T) with [(CSort _)
-\Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) (CHead c2 (Bind b) u) (CHead
-c (Bind b0) t) (clear_gen_bind b0 c (CHead c2 (Bind b) u) t H4)) in (\lambda
-(H9: (eq B b b0)).(\lambda (H10: (eq C c2 c)).(eq_ind_r T t (\lambda (t0:
-T).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d)
-t)) (CHead c1 (Bind b) (lift h d t0)))) (\lambda (c1: C).(drop h d c1 c2))))
-(eq_ind_r C c (\lambda (c0: C).(ex2 C (\lambda (c1: C).(clear (CHead x (Bind
-b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind b) (lift h d t)))) (\lambda
-(c1: C).(drop h d c1 c0)))) (eq_ind_r B b0 (\lambda (b1: B).(ex2 C (\lambda
-(c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind
-b1) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c)))) (ex_intro2 C (\lambda
-(c1: C).(clear (CHead x (Bind b0) (lift h (r (Bind b0) d) t)) (CHead c1 (Bind
-b0) (lift h d t)))) (\lambda (c1: C).(drop h d c1 c)) x (clear_bind b0 x
-(lift h d t)) H5) b H9) c2 H10) u H8)))) H7)) H6))))) (\lambda (f:
+ \lambda (x2: C).(let TMP_6 \def (\lambda (c: C).(\forall (x1: C).(\forall
+(h: nat).(\forall (d: nat).((drop h (S d) x1 c) \to (\forall (b: B).(\forall
+(c2: C).(\forall (u: T).((clear c (CHead c2 (Bind b) u)) \to (let TMP_4 \def
+(\lambda (c1: C).(let TMP_1 \def (Bind b) in (let TMP_2 \def (lift h d u) in
+(let TMP_3 \def (CHead c1 TMP_1 TMP_2) in (clear x1 TMP_3))))) in (let TMP_5
+\def (\lambda (c1: C).(drop h d c1 c2)) in (ex2 C TMP_4 TMP_5)))))))))))) in
+(let TMP_15 \def (\lambda (n: nat).(\lambda (x1: C).(\lambda (h:
+nat).(\lambda (d: nat).(\lambda (_: (drop h (S d) x1 (CSort n))).(\lambda (b:
+B).(\lambda (c2: C).(\lambda (u: T).(\lambda (H0: (clear (CSort n) (CHead c2
+(Bind b) u))).(let TMP_7 \def (Bind b) in (let TMP_8 \def (CHead c2 TMP_7 u)
+in (let TMP_12 \def (\lambda (c1: C).(let TMP_9 \def (Bind b) in (let TMP_10
+\def (lift h d u) in (let TMP_11 \def (CHead c1 TMP_9 TMP_10) in (clear x1
+TMP_11))))) in (let TMP_13 \def (\lambda (c1: C).(drop h d c1 c2)) in (let
+TMP_14 \def (ex2 C TMP_12 TMP_13) in (clear_gen_sort TMP_8 n H0
+TMP_14))))))))))))))) in (let TMP_162 \def (\lambda (c: C).(\lambda (H:
+((\forall (x1: C).(\forall (h: nat).(\forall (d: nat).((drop h (S d) x1 c)
+\to (\forall (b: B).(\forall (c2: C).(\forall (u: T).((clear c (CHead c2
+(Bind b) u)) \to (ex2 C (\lambda (c1: C).(clear x1 (CHead c1 (Bind b) (lift h
+d u)))) (\lambda (c1: C).(drop h d c1 c2))))))))))))).(\lambda (k:
+K).(\lambda (t: T).(\lambda (x1: C).(\lambda (h: nat).(\lambda (d:
+nat).(\lambda (H0: (drop h (S d) x1 (CHead c k t))).(\lambda (b: B).(\lambda
+(c2: C).(\lambda (u: T).(\lambda (H1: (clear (CHead c k t) (CHead c2 (Bind b)
+u))).(let TMP_19 \def (\lambda (e: C).(let TMP_16 \def (r k d) in (let TMP_17
+\def (lift h TMP_16 t) in (let TMP_18 \def (CHead e k TMP_17) in (eq C x1
+TMP_18))))) in (let TMP_21 \def (\lambda (e: C).(let TMP_20 \def (r k d) in
+(drop h TMP_20 e c))) in (let TMP_25 \def (\lambda (c1: C).(let TMP_22 \def
+(Bind b) in (let TMP_23 \def (lift h d u) in (let TMP_24 \def (CHead c1
+TMP_22 TMP_23) in (clear x1 TMP_24))))) in (let TMP_26 \def (\lambda (c1:
+C).(drop h d c1 c2)) in (let TMP_27 \def (ex2 C TMP_25 TMP_26) in (let
+TMP_160 \def (\lambda (x: C).(\lambda (H2: (eq C x1 (CHead x k (lift h (r k
+d) t)))).(\lambda (H3: (drop h (r k d) x c)).(let TMP_28 \def (r k d) in (let
+TMP_29 \def (lift h TMP_28 t) in (let TMP_30 \def (CHead x k TMP_29) in (let
+TMP_36 \def (\lambda (c0: C).(let TMP_34 \def (\lambda (c1: C).(let TMP_31
+\def (Bind b) in (let TMP_32 \def (lift h d u) in (let TMP_33 \def (CHead c1
+TMP_31 TMP_32) in (clear c0 TMP_33))))) in (let TMP_35 \def (\lambda (c1:
+C).(drop h d c1 c2)) in (ex2 C TMP_34 TMP_35)))) in (let TMP_45 \def (\lambda
+(k0: K).((clear (CHead c k0 t) (CHead c2 (Bind b) u)) \to ((drop h (r k0 d) x
+c) \to (let TMP_43 \def (\lambda (c1: C).(let TMP_37 \def (r k0 d) in (let
+TMP_38 \def (lift h TMP_37 t) in (let TMP_39 \def (CHead x k0 TMP_38) in (let
+TMP_40 \def (Bind b) in (let TMP_41 \def (lift h d u) in (let TMP_42 \def
+(CHead c1 TMP_40 TMP_41) in (clear TMP_39 TMP_42)))))))) in (let TMP_44 \def
+(\lambda (c1: C).(drop h d c1 c2)) in (ex2 C TMP_43 TMP_44)))))) in (let
+TMP_120 \def (\lambda (b0: B).(\lambda (H4: (clear (CHead c (Bind b0) t)
+(CHead c2 (Bind b) u))).(\lambda (H5: (drop h (r (Bind b0) d) x c)).(let
+TMP_46 \def (\lambda (e: C).(match e with [(CSort _) \Rightarrow c2 | (CHead
+c0 _ _) \Rightarrow c0])) in (let TMP_47 \def (Bind b) in (let TMP_48 \def
+(CHead c2 TMP_47 u) in (let TMP_49 \def (Bind b0) in (let TMP_50 \def (CHead
+c TMP_49 t) in (let TMP_51 \def (Bind b) in (let TMP_52 \def (CHead c2 TMP_51
+u) in (let TMP_53 \def (clear_gen_bind b0 c TMP_52 t H4) in (let H6 \def
+(f_equal C C TMP_46 TMP_48 TMP_50 TMP_53) in (let TMP_54 \def (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow b | (CHead _ k0 _) \Rightarrow (match
+k0 with [(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b])])) in (let
+TMP_55 \def (Bind b) in (let TMP_56 \def (CHead c2 TMP_55 u) in (let TMP_57
+\def (Bind b0) in (let TMP_58 \def (CHead c TMP_57 t) in (let TMP_59 \def
+(Bind b) in (let TMP_60 \def (CHead c2 TMP_59 u) in (let TMP_61 \def
+(clear_gen_bind b0 c TMP_60 t H4) in (let H7 \def (f_equal C B TMP_54 TMP_56
+TMP_58 TMP_61) in (let TMP_62 \def (\lambda (e: C).(match e with [(CSort _)
+\Rightarrow u | (CHead _ _ t0) \Rightarrow t0])) in (let TMP_63 \def (Bind b)
+in (let TMP_64 \def (CHead c2 TMP_63 u) in (let TMP_65 \def (Bind b0) in (let
+TMP_66 \def (CHead c TMP_65 t) in (let TMP_67 \def (Bind b) in (let TMP_68
+\def (CHead c2 TMP_67 u) in (let TMP_69 \def (clear_gen_bind b0 c TMP_68 t
+H4) in (let H8 \def (f_equal C T TMP_62 TMP_64 TMP_66 TMP_69) in (let TMP_118
+\def (\lambda (H9: (eq B b b0)).(\lambda (H10: (eq C c2 c)).(let TMP_80 \def
+(\lambda (t0: T).(let TMP_78 \def (\lambda (c1: C).(let TMP_70 \def (Bind b0)
+in (let TMP_71 \def (Bind b0) in (let TMP_72 \def (r TMP_71 d) in (let TMP_73
+\def (lift h TMP_72 t) in (let TMP_74 \def (CHead x TMP_70 TMP_73) in (let
+TMP_75 \def (Bind b) in (let TMP_76 \def (lift h d t0) in (let TMP_77 \def
+(CHead c1 TMP_75 TMP_76) in (clear TMP_74 TMP_77)))))))))) in (let TMP_79
+\def (\lambda (c1: C).(drop h d c1 c2)) in (ex2 C TMP_78 TMP_79)))) in (let
+TMP_91 \def (\lambda (c0: C).(let TMP_89 \def (\lambda (c1: C).(let TMP_81
+\def (Bind b0) in (let TMP_82 \def (Bind b0) in (let TMP_83 \def (r TMP_82 d)
+in (let TMP_84 \def (lift h TMP_83 t) in (let TMP_85 \def (CHead x TMP_81
+TMP_84) in (let TMP_86 \def (Bind b) in (let TMP_87 \def (lift h d t) in (let
+TMP_88 \def (CHead c1 TMP_86 TMP_87) in (clear TMP_85 TMP_88)))))))))) in
+(let TMP_90 \def (\lambda (c1: C).(drop h d c1 c0)) in (ex2 C TMP_89
+TMP_90)))) in (let TMP_102 \def (\lambda (b1: B).(let TMP_100 \def (\lambda
+(c1: C).(let TMP_92 \def (Bind b0) in (let TMP_93 \def (Bind b0) in (let
+TMP_94 \def (r TMP_93 d) in (let TMP_95 \def (lift h TMP_94 t) in (let TMP_96
+\def (CHead x TMP_92 TMP_95) in (let TMP_97 \def (Bind b1) in (let TMP_98
+\def (lift h d t) in (let TMP_99 \def (CHead c1 TMP_97 TMP_98) in (clear
+TMP_96 TMP_99)))))))))) in (let TMP_101 \def (\lambda (c1: C).(drop h d c1
+c)) in (ex2 C TMP_100 TMP_101)))) in (let TMP_111 \def (\lambda (c1: C).(let
+TMP_103 \def (Bind b0) in (let TMP_104 \def (Bind b0) in (let TMP_105 \def (r
+TMP_104 d) in (let TMP_106 \def (lift h TMP_105 t) in (let TMP_107 \def
+(CHead x TMP_103 TMP_106) in (let TMP_108 \def (Bind b0) in (let TMP_109 \def
+(lift h d t) in (let TMP_110 \def (CHead c1 TMP_108 TMP_109) in (clear
+TMP_107 TMP_110)))))))))) in (let TMP_112 \def (\lambda (c1: C).(drop h d c1
+c)) in (let TMP_113 \def (lift h d t) in (let TMP_114 \def (clear_bind b0 x
+TMP_113) in (let TMP_115 \def (ex_intro2 C TMP_111 TMP_112 x TMP_114 H5) in
+(let TMP_116 \def (eq_ind_r B b0 TMP_102 TMP_115 b H9) in (let TMP_117 \def
+(eq_ind_r C c TMP_91 TMP_116 c2 H10) in (eq_ind_r T t TMP_80 TMP_117 u
+H8))))))))))))) in (let TMP_119 \def (TMP_118 H7) in (TMP_119
+H6))))))))))))))))))))))))))))))))) in (let TMP_158 \def (\lambda (f: