-(let TMP_1 \def (\lambda (e0: C).(drop h O c e0)) in (let TMP_2 \def (\lambda
-(e0: C).(clear e0 e)) in (let TMP_3 \def (Flat f) in (let TMP_4 \def (CHead c
-TMP_3 u) in (let TMP_5 \def (getl h TMP_4 e) in (let TMP_26 \def (\lambda (x:
-C).(\lambda (H1: (drop h O c x)).(\lambda (H2: (clear x e)).(let TMP_8 \def
-(\lambda (n: nat).((drop n O c x) \to (let TMP_6 \def (Flat f) in (let TMP_7
-\def (CHead c TMP_6 u) in (getl n TMP_7 e))))) in (let TMP_19 \def (\lambda
-(H3: (drop O O c x)).(let TMP_9 \def (\lambda (c0: C).(clear c0 e)) in (let
-TMP_10 \def (drop_gen_refl c x H3) in (let H4 \def (eq_ind_r C x TMP_9 H2 c
-TMP_10) in (let TMP_11 \def (Flat f) in (let TMP_12 \def (CHead c TMP_11 u)
-in (let TMP_13 \def (Flat f) in (let TMP_14 \def (CHead c TMP_13 u) in (let
-TMP_15 \def (Flat f) in (let TMP_16 \def (CHead c TMP_15 u) in (let TMP_17
-\def (drop_refl TMP_16) in (let TMP_18 \def (clear_flat c e H4 f u) in
-(getl_intro O TMP_12 e TMP_14 TMP_17 TMP_18))))))))))))) in (let TMP_25 \def
-(\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)).(let TMP_20 \def (S h0) in
-(let TMP_21 \def (Flat f) in (let TMP_22 \def (CHead c TMP_21 u) in (let
-TMP_23 \def (Flat f) in (let TMP_24 \def (drop_drop TMP_23 h0 c x H3 u) in
-(getl_intro TMP_20 TMP_22 e x TMP_24 H2))))))))) in (nat_ind TMP_8 TMP_19
-TMP_25 h H1))))))) in (ex2_ind C TMP_1 TMP_2 TMP_5 TMP_26 H0))))))))))))).
+(ex2_ind C (\lambda (e0: C).(drop h O c e0)) (\lambda (e0: C).(clear e0 e))
+(getl h (CHead c (Flat f) u) e) (\lambda (x: C).(\lambda (H1: (drop h O c
+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))))))).