-C).(\lambda (c: C).(C_ind (\lambda (c0: C).((drop (S i0) O c0 a) \to (\forall
-(e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le (plus d
-h) (S i0)) \to (drop (minus (S i0) h) O e a)))))))) (\lambda (n:
-nat).(\lambda (H0: (drop (S i0) O (CSort n) a)).(\lambda (e: C).(\lambda (h:
-nat).(\lambda (d: nat).(\lambda (H1: (drop h d (CSort n) e)).(\lambda (H2:
-(le (plus d h) (S i0))).(and3_ind (eq C e (CSort n)) (eq nat h O) (eq nat d
-O) (drop (minus (S i0) h) O e a) (\lambda (H3: (eq C e (CSort n))).(\lambda
-(H4: (eq nat h O)).(\lambda (H5: (eq nat d O)).(and3_ind (eq C a (CSort n))
-(eq nat (S i0) O) (eq nat O O) (drop (minus (S i0) h) O e a) (\lambda (H6:
-(eq C a (CSort n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O
-O)).(let H9 \def (eq_ind nat d (\lambda (n0: nat).(le (plus n0 h) (S i0))) H2
-O H5) in (let H10 \def (eq_ind nat h (\lambda (n0: nat).(le (plus O n0) (S
-i0))) H9 O H4) in (eq_ind_r nat O (\lambda (n0: nat).(drop (minus (S i0) n0)
-O e a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O c0
-a)) (eq_ind_r C (CSort n) (\lambda (c0: C).(drop (minus (S i0) O) O (CSort n)
-c0)) (let H11 \def (eq_ind nat (S i0) (\lambda (ee: nat).(match ee in nat
-return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow
-True])) I O H7) in (False_ind (drop (minus (S i0) O) O (CSort n) (CSort n))
-H11)) a H6) e H3) h H4)))))) (drop_gen_sort n (S i0) O a H0)))))
-(drop_gen_sort n h d e H1))))))))) (\lambda (c0: C).(\lambda (H0: (((drop (S
-i0) O c0 a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h
-d c0 e) \to ((le (plus d h) (S i0)) \to (drop (minus (S i0) h) O e
-a))))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t: T).((drop (S
-i0) O (CHead c0 k0 t) a) \to (\forall (e: C).(\forall (h: nat).(\forall (d:
-nat).((drop h d (CHead c0 k0 t) e) \to ((le (plus d h) (S i0)) \to (drop
-(minus (S i0) h) O e a))))))))) (\lambda (b: B).(\lambda (t: T).(\lambda (H1:
-(drop (S i0) O (CHead c0 (Bind b) t) a)).(\lambda (e: C).(\lambda (h:
-nat).(\lambda (d: nat).(\lambda (H2: (drop h d (CHead c0 (Bind b) t)
-e)).(\lambda (H3: (le (plus d h) (S i0))).(nat_ind (\lambda (n: nat).((drop h
-n (CHead c0 (Bind b) t) e) \to ((le (plus n h) (S i0)) \to (drop (minus (S
-i0) h) O e a)))) (\lambda (H4: (drop h O (CHead c0 (Bind b) t) e)).(\lambda
-(H5: (le (plus O h) (S i0))).(nat_ind (\lambda (n: nat).((drop n O (CHead c0
-(Bind b) t) e) \to ((le (plus O n) (S i0)) \to (drop (minus (S i0) n) O e
-a)))) (\lambda (H6: (drop O O (CHead c0 (Bind b) t) e)).(\lambda (_: (le
-(plus O O) (S i0))).(eq_ind C (CHead c0 (Bind b) t) (\lambda (c1: C).(drop
-(minus (S i0) O) O c1 a)) (drop_drop (Bind b) i0 c0 a (drop_gen_drop (Bind b)
-c0 a t i0 H1) t) e (drop_gen_refl (CHead c0 (Bind b) t) e H6)))) (\lambda
-(h0: nat).(\lambda (_: (((drop h0 O (CHead c0 (Bind b) t) e) \to ((le (plus O
-h0) (S i0)) \to (drop (minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0)
-O (CHead c0 (Bind b) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(H a
-c0 (drop_gen_drop (Bind b) c0 a t i0 H1) e h0 O (drop_gen_drop (Bind b) c0 e
-t h0 H6) (le_S_n (plus O h0) i0 H7)))))) h H4 H5))) (\lambda (d0:
-nat).(\lambda (_: (((drop h d0 (CHead c0 (Bind b) t) e) \to ((le (plus d0 h)
-(S i0)) \to (drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0)
-(CHead c0 (Bind b) t) e)).(\lambda (H5: (le (plus (S d0) h) (S
-i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Bind
-b) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Bind b) d0)
-v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Bind b) d0) c0 e0))) (drop
-(minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C
-e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) d0)
-x1))).(\lambda (H8: (drop h (r (Bind b) d0) c0 x0)).(eq_ind_r C (CHead x0
-(Bind b) x1) (\lambda (c1: C).(drop (minus (S i0) h) O c1 a)) (eq_ind nat (S
-(minus i0 h)) (\lambda (n: nat).(drop n O (CHead x0 (Bind b) x1) a))
-(drop_drop (Bind b) (minus i0 h) x0 a (H a c0 (drop_gen_drop (Bind b) c0 a t
-i0 H1) x0 h d0 H8 (le_S_n (plus d0 h) i0 H5)) x1) (minus (S i0) h)
-(minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5)))) e
-H6)))))) (drop_gen_skip_l c0 e t h d0 (Bind b) H4)))))) d H2 H3)))))))))
-(\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c0 (Flat
-f) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2:
-(drop h d (CHead c0 (Flat f) t) e)).(\lambda (H3: (le (plus d h) (S
-i0))).(nat_ind (\lambda (n: nat).((drop h n (CHead c0 (Flat f) t) e) \to ((le
-(plus n h) (S i0)) \to (drop (minus (S i0) h) O e a)))) (\lambda (H4: (drop h
-O (CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus O h) (S i0))).(nat_ind
-(\lambda (n: nat).((drop n O (CHead c0 (Flat f) t) e) \to ((le (plus O n) (S
-i0)) \to (drop (minus (S i0) n) O e a)))) (\lambda (H6: (drop O O (CHead c0
-(Flat f) t) e)).(\lambda (_: (le (plus O O) (S i0))).(eq_ind C (CHead c0
-(Flat f) t) (\lambda (c1: C).(drop (minus (S i0) O) O c1 a)) (drop_drop (Flat
-f) i0 c0 a (drop_gen_drop (Flat f) c0 a t i0 H1) t) e (drop_gen_refl (CHead
-c0 (Flat f) t) e H6)))) (\lambda (h0: nat).(\lambda (_: (((drop h0 O (CHead
-c0 (Flat f) t) e) \to ((le (plus O h0) (S i0)) \to (drop (minus (S i0) h0) O
-e a))))).(\lambda (H6: (drop (S h0) O (CHead c0 (Flat f) t) e)).(\lambda (H7:
-(le (plus O (S h0)) (S i0))).(H0 (drop_gen_drop (Flat f) c0 a t i0 H1) e (S
-h0) O (drop_gen_drop (Flat f) c0 e t h0 H6) H7))))) h H4 H5))) (\lambda (d0:
-nat).(\lambda (_: (((drop h d0 (CHead c0 (Flat f) t) e) \to ((le (plus d0 h)
-(S i0)) \to (drop (minus (S i0) h) O e a))))).(\lambda (H4: (drop h (S d0)
-(CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus (S d0) h) (S
-i0))).(ex3_2_ind C T (\lambda (e0: C).(\lambda (v: T).(eq C e (CHead e0 (Flat
-f) v)))) (\lambda (_: C).(\lambda (v: T).(eq T t (lift h (r (Flat f) d0)
-v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Flat f) d0) c0 e0))) (drop
-(minus (S i0) h) O e a) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C
+C).(\lambda (c: C).(let TMP_26 \def (\lambda (c0: C).((drop (S i0) O c0 a)
+\to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to
+((le (plus d h) (S i0)) \to (let TMP_24 \def (S i0) in (let TMP_25 \def
+(minus TMP_24 h) in (drop TMP_25 O e a)))))))))) in (let TMP_75 \def (\lambda
+(n: nat).(\lambda (H0: (drop (S i0) O (CSort n) a)).(\lambda (e: C).(\lambda
+(h: nat).(\lambda (d: nat).(\lambda (H1: (drop h d (CSort n) e)).(\lambda
+(H2: (le (plus d h) (S i0))).(let TMP_27 \def (CSort n) in (let TMP_28 \def
+(eq C e TMP_27) in (let TMP_29 \def (eq nat h O) in (let TMP_30 \def (eq nat
+d O) in (let TMP_31 \def (S i0) in (let TMP_32 \def (minus TMP_31 h) in (let
+TMP_33 \def (drop TMP_32 O e a) in (let TMP_73 \def (\lambda (H3: (eq C e
+(CSort n))).(\lambda (H4: (eq nat h O)).(\lambda (H5: (eq nat d O)).(let
+TMP_34 \def (CSort n) in (let TMP_35 \def (eq C a TMP_34) in (let TMP_36 \def
+(S i0) in (let TMP_37 \def (eq nat TMP_36 O) in (let TMP_38 \def (eq nat O O)
+in (let TMP_39 \def (S i0) in (let TMP_40 \def (minus TMP_39 h) in (let
+TMP_41 \def (drop TMP_40 O e a) in (let TMP_70 \def (\lambda (H6: (eq C a
+(CSort n))).(\lambda (H7: (eq nat (S i0) O)).(\lambda (_: (eq nat O O)).(let
+TMP_44 \def (\lambda (n0: nat).(let TMP_42 \def (plus n0 h) in (let TMP_43
+\def (S i0) in (le TMP_42 TMP_43)))) in (let H9 \def (eq_ind nat d TMP_44 H2
+O H5) in (let TMP_47 \def (\lambda (n0: nat).(let TMP_45 \def (plus O n0) in
+(let TMP_46 \def (S i0) in (le TMP_45 TMP_46)))) in (let H10 \def (eq_ind nat
+h TMP_47 H9 O H4) in (let TMP_50 \def (\lambda (n0: nat).(let TMP_48 \def (S
+i0) in (let TMP_49 \def (minus TMP_48 n0) in (drop TMP_49 O e a)))) in (let
+TMP_51 \def (CSort n) in (let TMP_54 \def (\lambda (c0: C).(let TMP_52 \def
+(S i0) in (let TMP_53 \def (minus TMP_52 O) in (drop TMP_53 O c0 a)))) in
+(let TMP_55 \def (CSort n) in (let TMP_59 \def (\lambda (c0: C).(let TMP_56
+\def (S i0) in (let TMP_57 \def (minus TMP_56 O) in (let TMP_58 \def (CSort
+n) in (drop TMP_57 O TMP_58 c0))))) in (let TMP_60 \def (S i0) in (let TMP_61
+\def (\lambda (ee: nat).(match ee with [O \Rightarrow False | (S _)
+\Rightarrow True])) in (let H11 \def (eq_ind nat TMP_60 TMP_61 I O H7) in
+(let TMP_62 \def (S i0) in (let TMP_63 \def (minus TMP_62 O) in (let TMP_64
+\def (CSort n) in (let TMP_65 \def (CSort n) in (let TMP_66 \def (drop TMP_63
+O TMP_64 TMP_65) in (let TMP_67 \def (False_ind TMP_66 H11) in (let TMP_68
+\def (eq_ind_r C TMP_55 TMP_59 TMP_67 a H6) in (let TMP_69 \def (eq_ind_r C
+TMP_51 TMP_54 TMP_68 e H3) in (eq_ind_r nat O TMP_50 TMP_69 h
+H4)))))))))))))))))))))))) in (let TMP_71 \def (S i0) in (let TMP_72 \def
+(drop_gen_sort n TMP_71 O a H0) in (and3_ind TMP_35 TMP_37 TMP_38 TMP_41
+TMP_70 TMP_72))))))))))))))) in (let TMP_74 \def (drop_gen_sort n h d e H1)
+in (and3_ind TMP_28 TMP_29 TMP_30 TMP_33 TMP_73 TMP_74))))))))))))))))) in
+(let TMP_226 \def (\lambda (c0: C).(\lambda (H0: (((drop (S i0) O c0 a) \to
+(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h d c0 e) \to ((le
+(plus d h) (S i0)) \to (drop (minus (S i0) h) O e a))))))))).(\lambda (k:
+K).(let TMP_78 \def (\lambda (k0: K).(\forall (t: T).((drop (S i0) O (CHead
+c0 k0 t) a) \to (\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h
+d (CHead c0 k0 t) e) \to ((le (plus d h) (S i0)) \to (let TMP_76 \def (S i0)
+in (let TMP_77 \def (minus TMP_76 h) in (drop TMP_77 O e a))))))))))) in (let
+TMP_148 \def (\lambda (b: B).(\lambda (t: T).(\lambda (H1: (drop (S i0) O
+(CHead c0 (Bind b) t) a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d:
+nat).(\lambda (H2: (drop h d (CHead c0 (Bind b) t) e)).(\lambda (H3: (le
+(plus d h) (S i0))).(let TMP_81 \def (\lambda (n: nat).((drop h n (CHead c0
+(Bind b) t) e) \to ((le (plus n h) (S i0)) \to (let TMP_79 \def (S i0) in
+(let TMP_80 \def (minus TMP_79 h) in (drop TMP_80 O e a)))))) in (let TMP_105
+\def (\lambda (H4: (drop h O (CHead c0 (Bind b) t) e)).(\lambda (H5: (le
+(plus O h) (S i0))).(let TMP_84 \def (\lambda (n: nat).((drop n O (CHead c0
+(Bind b) t) e) \to ((le (plus O n) (S i0)) \to (let TMP_82 \def (S i0) in
+(let TMP_83 \def (minus TMP_82 n) in (drop TMP_83 O e a)))))) in (let TMP_97
+\def (\lambda (H6: (drop O O (CHead c0 (Bind b) t) e)).(\lambda (_: (le (plus
+O O) (S i0))).(let TMP_85 \def (Bind b) in (let TMP_86 \def (CHead c0 TMP_85
+t) in (let TMP_89 \def (\lambda (c1: C).(let TMP_87 \def (S i0) in (let
+TMP_88 \def (minus TMP_87 O) in (drop TMP_88 O c1 a)))) in (let TMP_90 \def
+(Bind b) in (let TMP_91 \def (Bind b) in (let TMP_92 \def (drop_gen_drop
+TMP_91 c0 a t i0 H1) in (let TMP_93 \def (drop_drop TMP_90 i0 c0 a TMP_92 t)
+in (let TMP_94 \def (Bind b) in (let TMP_95 \def (CHead c0 TMP_94 t) in (let
+TMP_96 \def (drop_gen_refl TMP_95 e H6) in (eq_ind C TMP_86 TMP_89 TMP_93 e
+TMP_96))))))))))))) in (let TMP_104 \def (\lambda (h0: nat).(\lambda (_:
+(((drop h0 O (CHead c0 (Bind b) t) e) \to ((le (plus O h0) (S i0)) \to (drop
+(minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0) O (CHead c0 (Bind b)
+t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(let TMP_98 \def (Bind b)
+in (let TMP_99 \def (drop_gen_drop TMP_98 c0 a t i0 H1) in (let TMP_100 \def
+(Bind b) in (let TMP_101 \def (drop_gen_drop TMP_100 c0 e t h0 H6) in (let
+TMP_102 \def (plus O h0) in (let TMP_103 \def (le_S_n TMP_102 i0 H7) in (H a
+c0 TMP_99 e h0 O TMP_101 TMP_103))))))))))) in (nat_ind TMP_84 TMP_97 TMP_104
+h H4 H5)))))) in (let TMP_147 \def (\lambda (d0: nat).(\lambda (_: (((drop h
+d0 (CHead c0 (Bind b) t) e) \to ((le (plus d0 h) (S i0)) \to (drop (minus (S
+i0) h) O e a))))).(\lambda (H4: (drop h (S d0) (CHead c0 (Bind b) t)
+e)).(\lambda (H5: (le (plus (S d0) h) (S i0))).(let TMP_108 \def (\lambda
+(e0: C).(\lambda (v: T).(let TMP_106 \def (Bind b) in (let TMP_107 \def
+(CHead e0 TMP_106 v) in (eq C e TMP_107))))) in (let TMP_112 \def (\lambda
+(_: C).(\lambda (v: T).(let TMP_109 \def (Bind b) in (let TMP_110 \def (r
+TMP_109 d0) in (let TMP_111 \def (lift h TMP_110 v) in (eq T t TMP_111))))))
+in (let TMP_115 \def (\lambda (e0: C).(\lambda (_: T).(let TMP_113 \def (Bind
+b) in (let TMP_114 \def (r TMP_113 d0) in (drop h TMP_114 c0 e0))))) in (let
+TMP_116 \def (S i0) in (let TMP_117 \def (minus TMP_116 h) in (let TMP_118
+\def (drop TMP_117 O e a) in (let TMP_144 \def (\lambda (x0: C).(\lambda (x1:
+T).(\lambda (H6: (eq C e (CHead x0 (Bind b) x1))).(\lambda (_: (eq T t (lift
+h (r (Bind b) d0) x1))).(\lambda (H8: (drop h (r (Bind b) d0) c0 x0)).(let
+TMP_119 \def (Bind b) in (let TMP_120 \def (CHead x0 TMP_119 x1) in (let
+TMP_123 \def (\lambda (c1: C).(let TMP_121 \def (S i0) in (let TMP_122 \def
+(minus TMP_121 h) in (drop TMP_122 O c1 a)))) in (let TMP_124 \def (minus i0
+h) in (let TMP_125 \def (S TMP_124) in (let TMP_128 \def (\lambda (n:
+nat).(let TMP_126 \def (Bind b) in (let TMP_127 \def (CHead x0 TMP_126 x1) in
+(drop n O TMP_127 a)))) in (let TMP_129 \def (Bind b) in (let TMP_130 \def
+(minus i0 h) in (let TMP_131 \def (Bind b) in (let TMP_132 \def
+(drop_gen_drop TMP_131 c0 a t i0 H1) in (let TMP_133 \def (plus d0 h) in (let
+TMP_134 \def (le_S_n TMP_133 i0 H5) in (let TMP_135 \def (H a c0 TMP_132 x0 h
+d0 H8 TMP_134) in (let TMP_136 \def (drop_drop TMP_129 TMP_130 x0 a TMP_135
+x1) in (let TMP_137 \def (S i0) in (let TMP_138 \def (minus TMP_137 h) in
+(let TMP_139 \def (plus d0 h) in (let TMP_140 \def (le_S_n TMP_139 i0 H5) in
+(let TMP_141 \def (le_trans_plus_r d0 h i0 TMP_140) in (let TMP_142 \def
+(minus_Sn_m i0 h TMP_141) in (let TMP_143 \def (eq_ind nat TMP_125 TMP_128
+TMP_136 TMP_138 TMP_142) in (eq_ind_r C TMP_120 TMP_123 TMP_143 e
+H6))))))))))))))))))))))))))) in (let TMP_145 \def (Bind b) in (let TMP_146
+\def (drop_gen_skip_l c0 e t h d0 TMP_145 H4) in (ex3_2_ind C T TMP_108
+TMP_112 TMP_115 TMP_118 TMP_144 TMP_146)))))))))))))) in (nat_ind TMP_81
+TMP_105 TMP_147 d H2 H3)))))))))))) in (let TMP_225 \def (\lambda (f:
+F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c0 (Flat f) t)
+a)).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H2: (drop h
+d (CHead c0 (Flat f) t) e)).(\lambda (H3: (le (plus d h) (S i0))).(let
+TMP_151 \def (\lambda (n: nat).((drop h n (CHead c0 (Flat f) t) e) \to ((le
+(plus n h) (S i0)) \to (let TMP_149 \def (S i0) in (let TMP_150 \def (minus
+TMP_149 h) in (drop TMP_150 O e a)))))) in (let TMP_174 \def (\lambda (H4:
+(drop h O (CHead c0 (Flat f) t) e)).(\lambda (H5: (le (plus O h) (S
+i0))).(let TMP_154 \def (\lambda (n: nat).((drop n O (CHead c0 (Flat f) t) e)
+\to ((le (plus O n) (S i0)) \to (let TMP_152 \def (S i0) in (let TMP_153 \def
+(minus TMP_152 n) in (drop TMP_153 O e a)))))) in (let TMP_167 \def (\lambda
+(H6: (drop O O (CHead c0 (Flat f) t) e)).(\lambda (_: (le (plus O O) (S
+i0))).(let TMP_155 \def (Flat f) in (let TMP_156 \def (CHead c0 TMP_155 t) in
+(let TMP_159 \def (\lambda (c1: C).(let TMP_157 \def (S i0) in (let TMP_158
+\def (minus TMP_157 O) in (drop TMP_158 O c1 a)))) in (let TMP_160 \def (Flat
+f) in (let TMP_161 \def (Flat f) in (let TMP_162 \def (drop_gen_drop TMP_161
+c0 a t i0 H1) in (let TMP_163 \def (drop_drop TMP_160 i0 c0 a TMP_162 t) in
+(let TMP_164 \def (Flat f) in (let TMP_165 \def (CHead c0 TMP_164 t) in (let
+TMP_166 \def (drop_gen_refl TMP_165 e H6) in (eq_ind C TMP_156 TMP_159
+TMP_163 e TMP_166))))))))))))) in (let TMP_173 \def (\lambda (h0:
+nat).(\lambda (_: (((drop h0 O (CHead c0 (Flat f) t) e) \to ((le (plus O h0)
+(S i0)) \to (drop (minus (S i0) h0) O e a))))).(\lambda (H6: (drop (S h0) O
+(CHead c0 (Flat f) t) e)).(\lambda (H7: (le (plus O (S h0)) (S i0))).(let
+TMP_168 \def (Flat f) in (let TMP_169 \def (drop_gen_drop TMP_168 c0 a t i0
+H1) in (let TMP_170 \def (S h0) in (let TMP_171 \def (Flat f) in (let TMP_172
+\def (drop_gen_drop TMP_171 c0 e t h0 H6) in (H0 TMP_169 e TMP_170 O TMP_172
+H7)))))))))) in (nat_ind TMP_154 TMP_167 TMP_173 h H4 H5)))))) in (let
+TMP_224 \def (\lambda (d0: nat).(\lambda (_: (((drop h d0 (CHead c0 (Flat f)
+t) e) \to ((le (plus d0 h) (S i0)) \to (drop (minus (S i0) h) O e
+a))))).(\lambda (H4: (drop h (S d0) (CHead c0 (Flat f) t) e)).(\lambda (H5:
+(le (plus (S d0) h) (S i0))).(let TMP_177 \def (\lambda (e0: C).(\lambda (v:
+T).(let TMP_175 \def (Flat f) in (let TMP_176 \def (CHead e0 TMP_175 v) in
+(eq C e TMP_176))))) in (let TMP_181 \def (\lambda (_: C).(\lambda (v:
+T).(let TMP_178 \def (Flat f) in (let TMP_179 \def (r TMP_178 d0) in (let
+TMP_180 \def (lift h TMP_179 v) in (eq T t TMP_180)))))) in (let TMP_184 \def
+(\lambda (e0: C).(\lambda (_: T).(let TMP_182 \def (Flat f) in (let TMP_183
+\def (r TMP_182 d0) in (drop h TMP_183 c0 e0))))) in (let TMP_185 \def (S i0)
+in (let TMP_186 \def (minus TMP_185 h) in (let TMP_187 \def (drop TMP_186 O e
+a) in (let TMP_221 \def (\lambda (x0: C).(\lambda (x1: T).(\lambda (H6: (eq C