-(Bind b0) w))).(let TMP_6 \def (\lambda (n: nat).((getl n (CHead c1 (Bind b)
-v) (CHead d1 (Bind b0) w)) \to (let TMP_5 \def (\lambda (d2: C).(let TMP_1
-\def (Bind b) in (let TMP_2 \def (CHead c2 TMP_1 v) in (let TMP_3 \def (Bind
-b0) in (let TMP_4 \def (CHead d2 TMP_3 w) in (getl n TMP_2 TMP_4)))))) in (ex
-C TMP_5)))) in (let TMP_68 \def (\lambda (H1: (getl O (CHead c1 (Bind b) v)
-(CHead d1 (Bind b0) w))).(let TMP_7 \def (\lambda (e: C).(match e with
-[(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) in (let TMP_8 \def
-(Bind b0) in (let TMP_9 \def (CHead d1 TMP_8 w) in (let TMP_10 \def (Bind b)
-in (let TMP_11 \def (CHead c1 TMP_10 v) in (let TMP_12 \def (Bind b0) in (let
-TMP_13 \def (CHead d1 TMP_12 w) in (let TMP_14 \def (Bind b) in (let TMP_15
-\def (CHead c1 TMP_14 v) in (let TMP_16 \def (Bind b0) in (let TMP_17 \def
-(CHead d1 TMP_16 w) in (let TMP_18 \def (getl_gen_O TMP_15 TMP_17 H1) in (let
-TMP_19 \def (clear_gen_bind b c1 TMP_13 v TMP_18) in (let H2 \def (f_equal C
-C TMP_7 TMP_9 TMP_11 TMP_19) in (let TMP_20 \def (\lambda (e: C).(match e
-with [(CSort _) \Rightarrow b0 | (CHead _ k _) \Rightarrow (match k with
-[(Bind b1) \Rightarrow b1 | (Flat _) \Rightarrow b0])])) in (let TMP_21 \def
-(Bind b0) in (let TMP_22 \def (CHead d1 TMP_21 w) in (let TMP_23 \def (Bind
-b) in (let TMP_24 \def (CHead c1 TMP_23 v) in (let TMP_25 \def (Bind b0) in
-(let TMP_26 \def (CHead d1 TMP_25 w) in (let TMP_27 \def (Bind b) in (let
-TMP_28 \def (CHead c1 TMP_27 v) in (let TMP_29 \def (Bind b0) in (let TMP_30
-\def (CHead d1 TMP_29 w) in (let TMP_31 \def (getl_gen_O TMP_28 TMP_30 H1) in
-(let TMP_32 \def (clear_gen_bind b c1 TMP_26 v TMP_31) in (let H3 \def
-(f_equal C B TMP_20 TMP_22 TMP_24 TMP_32) in (let TMP_33 \def (\lambda (e:
-C).(match e with [(CSort _) \Rightarrow w | (CHead _ _ t) \Rightarrow t])) in
-(let TMP_34 \def (Bind b0) in (let TMP_35 \def (CHead d1 TMP_34 w) in (let
-TMP_36 \def (Bind b) in (let TMP_37 \def (CHead c1 TMP_36 v) in (let TMP_38
-\def (Bind b0) in (let TMP_39 \def (CHead d1 TMP_38 w) in (let TMP_40 \def
-(Bind b) in (let TMP_41 \def (CHead c1 TMP_40 v) in (let TMP_42 \def (Bind
-b0) in (let TMP_43 \def (CHead d1 TMP_42 w) in (let TMP_44 \def (getl_gen_O
-TMP_41 TMP_43 H1) in (let TMP_45 \def (clear_gen_bind b c1 TMP_39 v TMP_44)
-in (let H4 \def (f_equal C T TMP_33 TMP_35 TMP_37 TMP_45) in (let TMP_66 \def
-(\lambda (H5: (eq B b0 b)).(\lambda (_: (eq C d1 c1)).(let TMP_51 \def
-(\lambda (t: T).(let TMP_50 \def (\lambda (d2: C).(let TMP_46 \def (Bind b)
-in (let TMP_47 \def (CHead c2 TMP_46 v) in (let TMP_48 \def (Bind b0) in (let
-TMP_49 \def (CHead d2 TMP_48 t) in (getl O TMP_47 TMP_49)))))) in (ex C
-TMP_50))) in (let TMP_57 \def (\lambda (b1: B).(let TMP_56 \def (\lambda (d2:
-C).(let TMP_52 \def (Bind b) in (let TMP_53 \def (CHead c2 TMP_52 v) in (let
-TMP_54 \def (Bind b1) in (let TMP_55 \def (CHead d2 TMP_54 v) in (getl O
-TMP_53 TMP_55)))))) in (ex C TMP_56))) in (let TMP_62 \def (\lambda (d2:
-C).(let TMP_58 \def (Bind b) in (let TMP_59 \def (CHead c2 TMP_58 v) in (let
-TMP_60 \def (Bind b) in (let TMP_61 \def (CHead d2 TMP_60 v) in (getl O
-TMP_59 TMP_61)))))) in (let TMP_63 \def (getl_refl b c2 v) in (let TMP_64
-\def (ex_intro C TMP_62 c2 TMP_63) in (let TMP_65 \def (eq_ind_r B b TMP_57
-TMP_64 b0 H5) in (eq_ind_r T v TMP_51 TMP_65 w H4))))))))) in (let TMP_67
-\def (TMP_66 H3) in (TMP_67 H2))))))))))))))))))))))))))))))))))))))))))))))
-in (let TMP_96 \def (\lambda (h0: nat).(\lambda (_: (((getl h0 (CHead c1
-(Bind b) v) (CHead d1 (Bind b0) w)) \to (ex C (\lambda (d2: C).(getl h0
-(CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))))))).(\lambda (H1: (getl (S h0)
-(CHead c1 (Bind b) v) (CHead d1 (Bind b0) w))).(let TMP_69 \def (Bind b) in
-(let TMP_70 \def (r TMP_69 h0) in (let TMP_71 \def (Bind b) in (let TMP_72
-\def (Bind b0) in (let TMP_73 \def (CHead d1 TMP_72 w) in (let TMP_74 \def
-(getl_gen_S TMP_71 c1 TMP_73 v h0 H1) in (let H_x \def (H b0 d1 w TMP_70
-TMP_74) in (let H2 \def H_x in (let TMP_77 \def (\lambda (d2: C).(let TMP_75
-\def (Bind b0) in (let TMP_76 \def (CHead d2 TMP_75 w) in (getl h0 c2
-TMP_76)))) in (let TMP_83 \def (\lambda (d2: C).(let TMP_78 \def (S h0) in
-(let TMP_79 \def (Bind b) in (let TMP_80 \def (CHead c2 TMP_79 v) in (let
-TMP_81 \def (Bind b0) in (let TMP_82 \def (CHead d2 TMP_81 w) in (getl TMP_78
-TMP_80 TMP_82))))))) in (let TMP_84 \def (ex C TMP_83) in (let TMP_95 \def
-(\lambda (x: C).(\lambda (H3: (getl h0 c2 (CHead x (Bind b0) w))).(let TMP_90
-\def (\lambda (d2: C).(let TMP_85 \def (S h0) in (let TMP_86 \def (Bind b) in
-(let TMP_87 \def (CHead c2 TMP_86 v) in (let TMP_88 \def (Bind b0) in (let
-TMP_89 \def (CHead d2 TMP_88 w) in (getl TMP_85 TMP_87 TMP_89))))))) in (let
-TMP_91 \def (Bind b) in (let TMP_92 \def (Bind b0) in (let TMP_93 \def (CHead
-x TMP_92 w) in (let TMP_94 \def (getl_head TMP_91 h0 c2 TMP_93 H3 v) in
-(ex_intro C TMP_90 x TMP_94)))))))) in (ex_ind C TMP_77 TMP_84 TMP_95
-H2)))))))))))))))) in (nat_ind TMP_6 TMP_68 TMP_96 h H0))))))))))))).
+(Bind b0) w))).(nat_ind (\lambda (n: nat).((getl n (CHead c1 (Bind b) v)
+(CHead d1 (Bind b0) w)) \to (ex C (\lambda (d2: C).(getl n (CHead c2 (Bind b)
+v) (CHead d2 (Bind b0) w)))))) (\lambda (H1: (getl O (CHead c1 (Bind b) v)
+(CHead d1 (Bind b0) w))).(let H2 \def (f_equal C C (\lambda (e: C).(match e
+with [(CSort _) \Rightarrow d1 | (CHead c _ _) \Rightarrow c])) (CHead d1
+(Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1 (Bind b0)
+w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1))) in ((let
+H3 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow b0
+| (CHead _ k _) \Rightarrow (match k with [(Bind b1) \Rightarrow b1 | (Flat
+_) \Rightarrow b0])])) (CHead d1 (Bind b0) w) (CHead c1 (Bind b) v)
+(clear_gen_bind b c1 (CHead d1 (Bind b0) w) v (getl_gen_O (CHead c1 (Bind b)
+v) (CHead d1 (Bind b0) w) H1))) in ((let H4 \def (f_equal C T (\lambda (e:
+C).(match e with [(CSort _) \Rightarrow w | (CHead _ _ t) \Rightarrow t]))
+(CHead d1 (Bind b0) w) (CHead c1 (Bind b) v) (clear_gen_bind b c1 (CHead d1
+(Bind b0) w) v (getl_gen_O (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w) H1)))
+in (\lambda (H5: (eq B b0 b)).(\lambda (_: (eq C d1 c1)).(eq_ind_r T v
+(\lambda (t: T).(ex C (\lambda (d2: C).(getl O (CHead c2 (Bind b) v) (CHead
+d2 (Bind b0) t))))) (eq_ind_r B b (\lambda (b1: B).(ex C (\lambda (d2:
+C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b1) v))))) (ex_intro C
+(\lambda (d2: C).(getl O (CHead c2 (Bind b) v) (CHead d2 (Bind b) v))) c2
+(getl_refl b c2 v)) b0 H5) w H4)))) H3)) H2))) (\lambda (h0: nat).(\lambda
+(_: (((getl h0 (CHead c1 (Bind b) v) (CHead d1 (Bind b0) w)) \to (ex C
+(\lambda (d2: C).(getl h0 (CHead c2 (Bind b) v) (CHead d2 (Bind b0)
+w))))))).(\lambda (H1: (getl (S h0) (CHead c1 (Bind b) v) (CHead d1 (Bind b0)
+w))).(let H_x \def (H b0 d1 w (r (Bind b) h0) (getl_gen_S (Bind b) c1 (CHead
+d1 (Bind b0) w) v h0 H1)) in (let H2 \def H_x in (ex_ind C (\lambda (d2:
+C).(getl h0 c2 (CHead d2 (Bind b0) w))) (ex C (\lambda (d2: C).(getl (S h0)
+(CHead c2 (Bind b) v) (CHead d2 (Bind b0) w)))) (\lambda (x: C).(\lambda (H3:
+(getl h0 c2 (CHead x (Bind b0) w))).(ex_intro C (\lambda (d2: C).(getl (S h0)
+(CHead c2 (Bind b) v) (CHead d2 (Bind b0) w))) x (getl_head (Bind b) h0 c2
+(CHead x (Bind b0) w) H3 v)))) H2)))))) h H0)))))))))).