-(Bind b) t) e)).(let TMP_130 \def (\lambda (e0: C).(\lambda (v: T).(let
-TMP_128 \def (Bind b) in (let TMP_129 \def (CHead e0 TMP_128 v) in (eq C e
-TMP_129))))) in (let TMP_136 \def (\lambda (_: C).(\lambda (v: T).(let
-TMP_131 \def (Bind b) in (let TMP_132 \def (S i0) in (let TMP_133 \def (plus
-TMP_132 d) in (let TMP_134 \def (r TMP_131 TMP_133) in (let TMP_135 \def
-(lift h TMP_134 v) in (eq T t TMP_135)))))))) in (let TMP_141 \def (\lambda
-(e0: C).(\lambda (_: T).(let TMP_137 \def (Bind b) in (let TMP_138 \def (S
-i0) in (let TMP_139 \def (plus TMP_138 d) in (let TMP_140 \def (r TMP_137
-TMP_139) in (drop h TMP_140 c1 e0))))))) in (let TMP_144 \def (\lambda (v:
-T).(\lambda (_: C).(let TMP_142 \def (r k d) in (let TMP_143 \def (lift h
-TMP_142 v) in (eq T u TMP_143))))) in (let TMP_147 \def (\lambda (v:
-T).(\lambda (e0: C).(let TMP_145 \def (S i0) in (let TMP_146 \def (CHead e0 k
-v) in (drop TMP_145 O e TMP_146))))) in (let TMP_149 \def (\lambda (_:
-T).(\lambda (e0: C).(let TMP_148 \def (r k d) in (drop h TMP_148 c0 e0)))) in
-(let TMP_150 \def (ex3_2 T C TMP_144 TMP_147 TMP_149) in (let TMP_198 \def
-(\lambda (x0: C).(\lambda (x1: T).(\lambda (H3: (eq C e (CHead x0 (Bind b)
-x1))).(\lambda (_: (eq T t (lift h (r (Bind b) (plus (S i0) d))
-x1))).(\lambda (H5: (drop h (r (Bind b) (plus (S i0) d)) c1 x0)).(let TMP_151
-\def (Bind b) in (let TMP_152 \def (CHead x0 TMP_151 x1) in (let TMP_161 \def
-(\lambda (c2: C).(let TMP_155 \def (\lambda (v: T).(\lambda (_: C).(let
-TMP_153 \def (r k d) in (let TMP_154 \def (lift h TMP_153 v) in (eq T u
-TMP_154))))) in (let TMP_158 \def (\lambda (v: T).(\lambda (e0: C).(let
-TMP_156 \def (S i0) in (let TMP_157 \def (CHead e0 k v) in (drop TMP_156 O c2
-TMP_157))))) in (let TMP_160 \def (\lambda (_: T).(\lambda (e0: C).(let
-TMP_159 \def (r k d) in (drop h TMP_159 c0 e0)))) in (ex3_2 T C TMP_155
-TMP_158 TMP_160))))) in (let TMP_162 \def (Bind b) in (let TMP_163 \def
-(CHead c0 k u) in (let TMP_164 \def (drop_gen_drop TMP_162 c1 TMP_163 t i0
-H1) in (let H6 \def (H u c0 c1 TMP_164 x0 h d H5) in (let TMP_167 \def
-(\lambda (v: T).(\lambda (_: C).(let TMP_165 \def (r k d) in (let TMP_166
-\def (lift h TMP_165 v) in (eq T u TMP_166))))) in (let TMP_169 \def (\lambda
-(v: T).(\lambda (e0: C).(let TMP_168 \def (CHead e0 k v) in (drop i0 O x0
-TMP_168)))) in (let TMP_171 \def (\lambda (_: T).(\lambda (e0: C).(let
-TMP_170 \def (r k d) in (drop h TMP_170 c0 e0)))) in (let TMP_174 \def
-(\lambda (v: T).(\lambda (_: C).(let TMP_172 \def (r k d) in (let TMP_173
-\def (lift h TMP_172 v) in (eq T u TMP_173))))) in (let TMP_179 \def (\lambda
-(v: T).(\lambda (e0: C).(let TMP_175 \def (S i0) in (let TMP_176 \def (Bind
-b) in (let TMP_177 \def (CHead x0 TMP_176 x1) in (let TMP_178 \def (CHead e0
-k v) in (drop TMP_175 O TMP_177 TMP_178))))))) in (let TMP_181 \def (\lambda
-(_: T).(\lambda (e0: C).(let TMP_180 \def (r k d) in (drop h TMP_180 c0
-e0)))) in (let TMP_182 \def (ex3_2 T C TMP_174 TMP_179 TMP_181) in (let
-TMP_196 \def (\lambda (x2: T).(\lambda (x3: C).(\lambda (H7: (eq T u (lift h
-(r k d) x2))).(\lambda (H8: (drop i0 O x0 (CHead x3 k x2))).(\lambda (H9:
-(drop h (r k d) c0 x3)).(let TMP_185 \def (\lambda (v: T).(\lambda (_:
-C).(let TMP_183 \def (r k d) in (let TMP_184 \def (lift h TMP_183 v) in (eq T
-u TMP_184))))) in (let TMP_190 \def (\lambda (v: T).(\lambda (e0: C).(let
-TMP_186 \def (S i0) in (let TMP_187 \def (Bind b) in (let TMP_188 \def (CHead
-x0 TMP_187 x1) in (let TMP_189 \def (CHead e0 k v) in (drop TMP_186 O TMP_188
-TMP_189))))))) in (let TMP_192 \def (\lambda (_: T).(\lambda (e0: C).(let
-TMP_191 \def (r k d) in (drop h TMP_191 c0 e0)))) in (let TMP_193 \def (Bind
-b) in (let TMP_194 \def (CHead x3 k x2) in (let TMP_195 \def (drop_drop
-TMP_193 i0 x0 TMP_194 H8 x1) in (ex3_2_intro T C TMP_185 TMP_190 TMP_192 x2
-x3 H7 TMP_195 H9)))))))))))) in (let TMP_197 \def (ex3_2_ind T C TMP_167
-TMP_169 TMP_171 TMP_182 TMP_196 H6) in (eq_ind_r C TMP_152 TMP_161 TMP_197 e
-H3)))))))))))))))))))))) in (let TMP_199 \def (S i0) in (let TMP_200 \def
-(plus TMP_199 d) in (let TMP_201 \def (Bind b) in (let TMP_202 \def
-(drop_gen_skip_l c1 e t h TMP_200 TMP_201 H2) in (ex3_2_ind C T TMP_130
-TMP_136 TMP_141 TMP_150 TMP_198 TMP_202)))))))))))))))))))) in (let TMP_281
-\def (\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c1
-(Flat f) t) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d:
-nat).(\lambda (H2: (drop h (S (plus (S i0) d)) (CHead c1 (Flat f) t) e)).(let
-TMP_206 \def (\lambda (e0: C).(\lambda (v: T).(let TMP_204 \def (Flat f) in
-(let TMP_205 \def (CHead e0 TMP_204 v) in (eq C e TMP_205))))) in (let
-TMP_212 \def (\lambda (_: C).(\lambda (v: T).(let TMP_207 \def (Flat f) in
-(let TMP_208 \def (S i0) in (let TMP_209 \def (plus TMP_208 d) in (let
-TMP_210 \def (r TMP_207 TMP_209) in (let TMP_211 \def (lift h TMP_210 v) in
-(eq T t TMP_211)))))))) in (let TMP_217 \def (\lambda (e0: C).(\lambda (_:
-T).(let TMP_213 \def (Flat f) in (let TMP_214 \def (S i0) in (let TMP_215
-\def (plus TMP_214 d) in (let TMP_216 \def (r TMP_213 TMP_215) in (drop h
-TMP_216 c1 e0))))))) in (let TMP_220 \def (\lambda (v: T).(\lambda (_:
-C).(let TMP_218 \def (r k d) in (let TMP_219 \def (lift h TMP_218 v) in (eq T
-u TMP_219))))) in (let TMP_223 \def (\lambda (v: T).(\lambda (e0: C).(let
-TMP_221 \def (S i0) in (let TMP_222 \def (CHead e0 k v) in (drop TMP_221 O e
-TMP_222))))) in (let TMP_225 \def (\lambda (_: T).(\lambda (e0: C).(let
-TMP_224 \def (r k d) in (drop h TMP_224 c0 e0)))) in (let TMP_226 \def (ex3_2
-T C TMP_220 TMP_223 TMP_225) in (let TMP_276 \def (\lambda (x0: C).(\lambda
-(x1: T).(\lambda (H3: (eq C e (CHead x0 (Flat f) x1))).(\lambda (_: (eq T t
-(lift h (r (Flat f) (plus (S i0) d)) x1))).(\lambda (H5: (drop h (r (Flat f)
-(plus (S i0) d)) c1 x0)).(let TMP_227 \def (Flat f) in (let TMP_228 \def
-(CHead x0 TMP_227 x1) in (let TMP_237 \def (\lambda (c2: C).(let TMP_231 \def
-(\lambda (v: T).(\lambda (_: C).(let TMP_229 \def (r k d) in (let TMP_230
-\def (lift h TMP_229 v) in (eq T u TMP_230))))) in (let TMP_234 \def (\lambda
-(v: T).(\lambda (e0: C).(let TMP_232 \def (S i0) in (let TMP_233 \def (CHead
-e0 k v) in (drop TMP_232 O c2 TMP_233))))) in (let TMP_236 \def (\lambda (_:
-T).(\lambda (e0: C).(let TMP_235 \def (r k d) in (drop h TMP_235 c0 e0)))) in
-(ex3_2 T C TMP_231 TMP_234 TMP_236))))) in (let TMP_240 \def (\lambda (v:
-T).(\lambda (_: C).(let TMP_238 \def (r k d) in (let TMP_239 \def (lift h
-TMP_238 v) in (eq T u TMP_239))))) in (let TMP_243 \def (\lambda (v:
-T).(\lambda (e0: C).(let TMP_241 \def (S i0) in (let TMP_242 \def (CHead e0 k
-v) in (drop TMP_241 O x0 TMP_242))))) in (let TMP_245 \def (\lambda (_:
-T).(\lambda (e0: C).(let TMP_244 \def (r k d) in (drop h TMP_244 c0 e0)))) in
-(let TMP_248 \def (\lambda (v: T).(\lambda (_: C).(let TMP_246 \def (r k d)
-in (let TMP_247 \def (lift h TMP_246 v) in (eq T u TMP_247))))) in (let
-TMP_253 \def (\lambda (v: T).(\lambda (e0: C).(let TMP_249 \def (S i0) in
-(let TMP_250 \def (Flat f) in (let TMP_251 \def (CHead x0 TMP_250 x1) in (let
-TMP_252 \def (CHead e0 k v) in (drop TMP_249 O TMP_251 TMP_252))))))) in (let
-TMP_255 \def (\lambda (_: T).(\lambda (e0: C).(let TMP_254 \def (r k d) in
-(drop h TMP_254 c0 e0)))) in (let TMP_256 \def (ex3_2 T C TMP_248 TMP_253
-TMP_255) in (let TMP_270 \def (\lambda (x2: T).(\lambda (x3: C).(\lambda (H6:
-(eq T u (lift h (r k d) x2))).(\lambda (H7: (drop (S i0) O x0 (CHead x3 k
-x2))).(\lambda (H8: (drop h (r k d) c0 x3)).(let TMP_259 \def (\lambda (v:
-T).(\lambda (_: C).(let TMP_257 \def (r k d) in (let TMP_258 \def (lift h
-TMP_257 v) in (eq T u TMP_258))))) in (let TMP_264 \def (\lambda (v:
-T).(\lambda (e0: C).(let TMP_260 \def (S i0) in (let TMP_261 \def (Flat f) in
-(let TMP_262 \def (CHead x0 TMP_261 x1) in (let TMP_263 \def (CHead e0 k v)
-in (drop TMP_260 O TMP_262 TMP_263))))))) in (let TMP_266 \def (\lambda (_:
-T).(\lambda (e0: C).(let TMP_265 \def (r k d) in (drop h TMP_265 c0 e0)))) in
-(let TMP_267 \def (Flat f) in (let TMP_268 \def (CHead x3 k x2) in (let
-TMP_269 \def (drop_drop TMP_267 i0 x0 TMP_268 H7 x1) in (ex3_2_intro T C
-TMP_259 TMP_264 TMP_266 x2 x3 H6 TMP_269 H8)))))))))))) in (let TMP_271 \def
-(Flat f) in (let TMP_272 \def (CHead c0 k u) in (let TMP_273 \def
-(drop_gen_drop TMP_271 c1 TMP_272 t i0 H1) in (let TMP_274 \def (H0 TMP_273
-x0 h d H5) in (let TMP_275 \def (ex3_2_ind T C TMP_240 TMP_243 TMP_245
-TMP_256 TMP_270 TMP_274) in (eq_ind_r C TMP_228 TMP_237 TMP_275 e
-H3)))))))))))))))))))))) in (let TMP_277 \def (S i0) in (let TMP_278 \def
-(plus TMP_277 d) in (let TMP_279 \def (Flat f) in (let TMP_280 \def
-(drop_gen_skip_l c1 e t h TMP_278 TMP_279 H2) in (ex3_2_ind C T TMP_206
-TMP_212 TMP_217 TMP_226 TMP_276 TMP_280)))))))))))))))))))) in (K_ind TMP_127
-TMP_203 TMP_281 k0))))))) in (C_ind TMP_83 TMP_118 TMP_282 c))))))))) in
-(nat_ind TMP_8 TMP_74 TMP_283 i))))).
+(Bind b) t) e)).(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) (plus (S i0) d)) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r
+(Bind b) (plus (S i0) d)) c1 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_:
+C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S
+i0) O e (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0
+e0)))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H3: (eq C e (CHead x0
+(Bind b) x1))).(\lambda (_: (eq T t (lift h (r (Bind b) (plus (S i0) d))
+x1))).(\lambda (H5: (drop h (r (Bind b) (plus (S i0) d)) c1 x0)).(eq_ind_r C
+(CHead x0 (Bind b) x1) (\lambda (c2: C).(ex3_2 T C (\lambda (v: T).(\lambda
+(_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop
+(S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k
+d) c0 e0))))) (let H6 \def (H u c0 c1 (drop_gen_drop (Bind b) c1 (CHead c0 k
+u) t i0 H1) x0 h d H5) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq
+T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop i0 O x0
+(CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))
+(ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v))))
+(\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Bind b) x1) (CHead
+e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))))
+(\lambda (x2: T).(\lambda (x3: C).(\lambda (H7: (eq T u (lift h (r k d)
+x2))).(\lambda (H8: (drop i0 O x0 (CHead x3 k x2))).(\lambda (H9: (drop h (r
+k d) c0 x3)).(ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h
+(r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Bind
+b) x1) (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0
+e0))) x2 x3 H7 (drop_drop (Bind b) i0 x0 (CHead x3 k x2) H8 x1) H9)))))) H6))
+e H3)))))) (drop_gen_skip_l c1 e t h (plus (S i0) d) (Bind b) H2)))))))))
+(\lambda (f: F).(\lambda (t: T).(\lambda (H1: (drop (S i0) O (CHead c1 (Flat
+f) t) (CHead c0 k u))).(\lambda (e: C).(\lambda (h: nat).(\lambda (d:
+nat).(\lambda (H2: (drop h (S (plus (S i0) d)) (CHead c1 (Flat f) t)
+e)).(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) (plus (S
+i0) d)) v)))) (\lambda (e0: C).(\lambda (_: T).(drop h (r (Flat f) (plus (S
+i0) d)) c1 e0))) (ex3_2 T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h
+(r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O e (CHead e0 k
+v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda
+(x0: C).(\lambda (x1: T).(\lambda (H3: (eq C e (CHead x0 (Flat f)
+x1))).(\lambda (_: (eq T t (lift h (r (Flat f) (plus (S i0) d))
+x1))).(\lambda (H5: (drop h (r (Flat f) (plus (S i0) d)) c1 x0)).(eq_ind_r C
+(CHead x0 (Flat f) x1) (\lambda (c2: C).(ex3_2 T C (\lambda (v: T).(\lambda
+(_: C).(eq T u (lift h (r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop
+(S i0) O c2 (CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k
+d) c0 e0))))) (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h
+(r k d) v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O x0 (CHead e0 k
+v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0))) (ex3_2 T C
+(\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d) v)))) (\lambda (v:
+T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Flat f) x1) (CHead e0 k v))))
+(\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))) (\lambda (x2:
+T).(\lambda (x3: C).(\lambda (H6: (eq T u (lift h (r k d) x2))).(\lambda (H7:
+(drop (S i0) O x0 (CHead x3 k x2))).(\lambda (H8: (drop h (r k d) c0
+x3)).(ex3_2_intro T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (r k d)
+v)))) (\lambda (v: T).(\lambda (e0: C).(drop (S i0) O (CHead x0 (Flat f) x1)
+(CHead e0 k v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (r k d) c0 e0)))
+x2 x3 H6 (drop_drop (Flat f) i0 x0 (CHead x3 k x2) H7 x1) H8)))))) (H0
+(drop_gen_drop (Flat f) c1 (CHead c0 k u) t i0 H1) x0 h d H5)) e H3))))))
+(drop_gen_skip_l c1 e t h (plus (S i0) d) (Flat f) H2))))))))) k0)))) c))))))
+i)).