-(clear (CHead c3 k u) e1)).(let TMP_12 \def (\lambda (k0: K).((clear (CHead
-c3 k0 u) e1) \to (let TMP_9 \def (\lambda (e2: C).(csubt g e1 e2)) in (let
-TMP_11 \def (\lambda (e2: C).(let TMP_10 \def (CHead c4 k0 u) in (clear
-TMP_10 e2))) in (ex2 C TMP_9 TMP_11))))) in (let TMP_33 \def (\lambda (b:
-B).(\lambda (H3: (clear (CHead c3 (Bind b) u) e1)).(let TMP_13 \def (Bind b)
-in (let TMP_14 \def (CHead c3 TMP_13 u) in (let TMP_19 \def (\lambda (c:
-C).(let TMP_15 \def (\lambda (e2: C).(csubt g c e2)) in (let TMP_18 \def
-(\lambda (e2: C).(let TMP_16 \def (Bind b) in (let TMP_17 \def (CHead c4
-TMP_16 u) in (clear TMP_17 e2)))) in (ex2 C TMP_15 TMP_18)))) in (let TMP_22
-\def (\lambda (e2: C).(let TMP_20 \def (Bind b) in (let TMP_21 \def (CHead c3
-TMP_20 u) in (csubt g TMP_21 e2)))) in (let TMP_25 \def (\lambda (e2: C).(let
-TMP_23 \def (Bind b) in (let TMP_24 \def (CHead c4 TMP_23 u) in (clear TMP_24
-e2)))) in (let TMP_26 \def (Bind b) in (let TMP_27 \def (CHead c4 TMP_26 u)
-in (let TMP_28 \def (Bind b) in (let TMP_29 \def (csubt_head g c3 c4 H0
-TMP_28 u) in (let TMP_30 \def (clear_bind b c4 u) in (let TMP_31 \def
-(ex_intro2 C TMP_22 TMP_25 TMP_27 TMP_29 TMP_30) in (let TMP_32 \def
-(clear_gen_bind b c3 e1 u H3) in (eq_ind_r C TMP_14 TMP_19 TMP_31 e1
-TMP_32))))))))))))))) in (let TMP_48 \def (\lambda (f: F).(\lambda (H3:
-(clear (CHead c3 (Flat f) u) e1)).(let TMP_34 \def (clear_gen_flat f c3 e1 u
-H3) in (let H4 \def (H1 e1 TMP_34) in (let TMP_35 \def (\lambda (e2:
-C).(csubt g e1 e2)) in (let TMP_36 \def (\lambda (e2: C).(clear c4 e2)) in
-(let TMP_37 \def (\lambda (e2: C).(csubt g e1 e2)) in (let TMP_40 \def
-(\lambda (e2: C).(let TMP_38 \def (Flat f) in (let TMP_39 \def (CHead c4
-TMP_38 u) in (clear TMP_39 e2)))) in (let TMP_41 \def (ex2 C TMP_37 TMP_40)
-in (let TMP_47 \def (\lambda (x: C).(\lambda (H5: (csubt g e1 x)).(\lambda
-(H6: (clear c4 x)).(let TMP_42 \def (\lambda (e2: C).(csubt g e1 e2)) in (let
-TMP_45 \def (\lambda (e2: C).(let TMP_43 \def (Flat f) in (let TMP_44 \def
-(CHead c4 TMP_43 u) in (clear TMP_44 e2)))) in (let TMP_46 \def (clear_flat
-c4 x H6 f u) in (ex_intro2 C TMP_42 TMP_45 x H5 TMP_46))))))) in (ex2_ind C
-TMP_35 TMP_36 TMP_41 TMP_47 H4))))))))))) in (K_ind TMP_12 TMP_33 TMP_48 k
-H2)))))))))))) in (let TMP_69 \def (\lambda (c3: C).(\lambda (c4: C).(\lambda
-(H0: (csubt g c3 c4)).(\lambda (_: ((\forall (e1: C).((clear c3 e1) \to (ex2
-C (\lambda (e2: C).(csubt g e1 e2)) (\lambda (e2: C).(clear c4
-e2))))))).(\lambda (b: B).(\lambda (H2: (not (eq B b Void))).(\lambda (u1:
-T).(\lambda (u2: T).(\lambda (e1: C).(\lambda (H3: (clear (CHead c3 (Bind
-Void) u1) e1)).(let TMP_50 \def (Bind Void) in (let TMP_51 \def (CHead c3
-TMP_50 u1) in (let TMP_56 \def (\lambda (c: C).(let TMP_52 \def (\lambda (e2:
-C).(csubt g c e2)) in (let TMP_55 \def (\lambda (e2: C).(let TMP_53 \def
-(Bind b) in (let TMP_54 \def (CHead c4 TMP_53 u2) in (clear TMP_54 e2)))) in
-(ex2 C TMP_52 TMP_55)))) in (let TMP_59 \def (\lambda (e2: C).(let TMP_57
-\def (Bind Void) in (let TMP_58 \def (CHead c3 TMP_57 u1) in (csubt g TMP_58
-e2)))) in (let TMP_62 \def (\lambda (e2: C).(let TMP_60 \def (Bind b) in (let
-TMP_61 \def (CHead c4 TMP_60 u2) in (clear TMP_61 e2)))) in (let TMP_63 \def
-(Bind b) in (let TMP_64 \def (CHead c4 TMP_63 u2) in (let TMP_65 \def
-(csubt_void g c3 c4 H0 b H2 u1 u2) in (let TMP_66 \def (clear_bind b c4 u2)
-in (let TMP_67 \def (ex_intro2 C TMP_59 TMP_62 TMP_64 TMP_65 TMP_66) in (let
-TMP_68 \def (clear_gen_bind Void c3 e1 u1 H3) in (eq_ind_r C TMP_51 TMP_56
-TMP_67 e1 TMP_68)))))))))))))))))))))) in (let TMP_89 \def (\lambda (c3:
+(clear (CHead c3 k u) e1)).(K_ind (\lambda (k0: K).((clear (CHead c3 k0 u)
+e1) \to (ex2 C (\lambda (e2: C).(csubt g e1 e2)) (\lambda (e2: C).(clear
+(CHead c4 k0 u) e2))))) (\lambda (b: B).(\lambda (H3: (clear (CHead c3 (Bind
+b) u) e1)).(eq_ind_r C (CHead c3 (Bind b) u) (\lambda (c: C).(ex2 C (\lambda
+(e2: C).(csubt g c e2)) (\lambda (e2: C).(clear (CHead c4 (Bind b) u) e2))))
+(ex_intro2 C (\lambda (e2: C).(csubt g (CHead c3 (Bind b) u) e2)) (\lambda
+(e2: C).(clear (CHead c4 (Bind b) u) e2)) (CHead c4 (Bind b) u) (csubt_head g
+c3 c4 H0 (Bind b) u) (clear_bind b c4 u)) e1 (clear_gen_bind b c3 e1 u H3))))
+(\lambda (f: F).(\lambda (H3: (clear (CHead c3 (Flat f) u) e1)).(let H4 \def
+(H1 e1 (clear_gen_flat f c3 e1 u H3)) in (ex2_ind C (\lambda (e2: C).(csubt g
+e1 e2)) (\lambda (e2: C).(clear c4 e2)) (ex2 C (\lambda (e2: C).(csubt g e1
+e2)) (\lambda (e2: C).(clear (CHead c4 (Flat f) u) e2))) (\lambda (x:
+C).(\lambda (H5: (csubt g e1 x)).(\lambda (H6: (clear c4 x)).(ex_intro2 C
+(\lambda (e2: C).(csubt g e1 e2)) (\lambda (e2: C).(clear (CHead c4 (Flat f)
+u) e2)) x H5 (clear_flat c4 x H6 f u))))) H4)))) k H2))))))))) (\lambda (c3: