-x)).(\lambda (H2: (clear x e)).((match h in nat return (\lambda (n:
-nat).((drop n O c x) \to (getl n (CHead c (Flat f) u) e))) with [O
-\Rightarrow (\lambda (H3: (drop O O c x)).(let H4 \def (eq_ind_r C x (\lambda
-(c: C).(clear c e)) H2 c (drop_gen_refl c x H3)) in (getl_intro O (CHead c
-(Flat f) u) e (CHead c (Flat f) u) (drop_refl (CHead c (Flat f) u))
-(clear_flat c e H4 f u)))) | (S n) \Rightarrow (\lambda (H3: (drop (S n) O c
-x)).(getl_intro (S n) (CHead c (Flat f) u) e x (drop_drop (Flat f) n c x H3
-u) H2))]) H1)))) H0))))))).
+x)).(\lambda (H2: (clear x e)).(nat_ind (\lambda (n: nat).((drop n O c x) \to
+(getl n (CHead c (Flat f) u) e))) (\lambda (H3: (drop O O c x)).(let H4 \def
+(eq_ind_r C x (\lambda (c0: C).(clear c0 e)) H2 c (drop_gen_refl c x H3)) in
+(getl_intro O (CHead c (Flat f) u) e (CHead c (Flat f) u) (drop_refl (CHead c
+(Flat f) u)) (clear_flat c e H4 f u)))) (\lambda (h0: nat).(\lambda (_:
+(((drop h0 O c x) \to (getl h0 (CHead c (Flat f) u) e)))).(\lambda (H3: (drop
+(S h0) O c x)).(getl_intro (S h0) (CHead c (Flat f) u) e x (drop_drop (Flat
+f) h0 c x H3 u) H2)))) h H1)))) H0))))))).