-nat).(let TMP_10 \def (\lambda (n: nat).((getl n (CHead e (Bind b) v) d) \to
-(let TMP_1 \def (eq nat n O) in (let TMP_2 \def (Bind b) in (let TMP_3 \def
-(CHead e TMP_2 v) in (let TMP_4 \def (eq C d TMP_3) in (let TMP_5 \def (land
-TMP_1 TMP_4) in (let TMP_7 \def (\lambda (j: nat).(let TMP_6 \def (S j) in
-(eq nat n TMP_6))) in (let TMP_8 \def (\lambda (j: nat).(getl j e d)) in (let
-TMP_9 \def (ex2 nat TMP_7 TMP_8) in (or TMP_5 TMP_9))))))))))) in (let TMP_52
-\def (\lambda (H: (getl O (CHead e (Bind b) v) d)).(let TMP_11 \def (Bind b)
-in (let TMP_12 \def (CHead e TMP_11 v) in (let TMP_22 \def (\lambda (c:
-C).(let TMP_13 \def (eq nat O O) in (let TMP_14 \def (Bind b) in (let TMP_15
-\def (CHead e TMP_14 v) in (let TMP_16 \def (eq C c TMP_15) in (let TMP_17
-\def (land TMP_13 TMP_16) in (let TMP_19 \def (\lambda (j: nat).(let TMP_18
-\def (S j) in (eq nat O TMP_18))) in (let TMP_20 \def (\lambda (j: nat).(getl
-j e c)) in (let TMP_21 \def (ex2 nat TMP_19 TMP_20) in (or TMP_17
-TMP_21)))))))))) in (let TMP_23 \def (eq nat O O) in (let TMP_24 \def (Bind
-b) in (let TMP_25 \def (CHead e TMP_24 v) in (let TMP_26 \def (Bind b) in
-(let TMP_27 \def (CHead e TMP_26 v) in (let TMP_28 \def (eq C TMP_25 TMP_27)
-in (let TMP_29 \def (land TMP_23 TMP_28) in (let TMP_31 \def (\lambda (j:
-nat).(let TMP_30 \def (S j) in (eq nat O TMP_30))) in (let TMP_34 \def
-(\lambda (j: nat).(let TMP_32 \def (Bind b) in (let TMP_33 \def (CHead e
-TMP_32 v) in (getl j e TMP_33)))) in (let TMP_35 \def (ex2 nat TMP_31 TMP_34)
-in (let TMP_36 \def (eq nat O O) in (let TMP_37 \def (Bind b) in (let TMP_38
-\def (CHead e TMP_37 v) in (let TMP_39 \def (Bind b) in (let TMP_40 \def
-(CHead e TMP_39 v) in (let TMP_41 \def (eq C TMP_38 TMP_40) in (let TMP_42
-\def (refl_equal nat O) in (let TMP_43 \def (Bind b) in (let TMP_44 \def
-(CHead e TMP_43 v) in (let TMP_45 \def (refl_equal C TMP_44) in (let TMP_46
-\def (conj TMP_36 TMP_41 TMP_42 TMP_45) in (let TMP_47 \def (or_introl TMP_29
-TMP_35 TMP_46) in (let TMP_48 \def (Bind b) in (let TMP_49 \def (CHead e
-TMP_48 v) in (let TMP_50 \def (getl_gen_O TMP_49 d H) in (let TMP_51 \def
-(clear_gen_bind b e d v TMP_50) in (eq_ind_r C TMP_12 TMP_22 TMP_47 d
-TMP_51))))))))))))))))))))))))))))))) in (let TMP_73 \def (\lambda (n:
+nat).(nat_ind (\lambda (n: nat).((getl n (CHead e (Bind b) v) d) \to (or
+(land (eq nat n O) (eq C d (CHead e (Bind b) v))) (ex2 nat (\lambda (j:
+nat).(eq nat n (S j))) (\lambda (j: nat).(getl j e d)))))) (\lambda (H: (getl
+O (CHead e (Bind b) v) d)).(eq_ind_r C (CHead e (Bind b) v) (\lambda (c:
+C).(or (land (eq nat O O) (eq C c (CHead e (Bind b) v))) (ex2 nat (\lambda
+(j: nat).(eq nat O (S j))) (\lambda (j: nat).(getl j e c))))) (or_introl
+(land (eq nat O O) (eq C (CHead e (Bind b) v) (CHead e (Bind b) v))) (ex2 nat
+(\lambda (j: nat).(eq nat O (S j))) (\lambda (j: nat).(getl j e (CHead e
+(Bind b) v)))) (conj (eq nat O O) (eq C (CHead e (Bind b) v) (CHead e (Bind
+b) v)) (refl_equal nat O) (refl_equal C (CHead e (Bind b) v)))) d
+(clear_gen_bind b e d v (getl_gen_O (CHead e (Bind b) v) d H)))) (\lambda (n: