-b0) w0)))) (\lambda (x0: C).(\lambda (H5: (getl (plus (S h) i) c2 (CHead x0
-(Bind b0) w0))).(let H_y0 \def (getl_conf_le (plus (S h) i) (CHead x0 (Bind
-b0) w0) c2 H5 (CHead x (Bind b) w) i H2) in (let H6 \def (eq_ind nat (minus
-(plus (S h) i) i) (\lambda (n: nat).(getl n (CHead x (Bind b) w) (CHead x0
-(Bind b0) w0))) (H_y0 (le_plus_r (S h) i)) (S h) (minus_plus_r (S h) i)) in
-(ex_intro C (\lambda (d2: C).(getl h x (CHead d2 (Bind b0) w0))) x0
-(getl_gen_S (Bind b) x (CHead x0 (Bind b0) w0) w h H6)))))) H4))))))))) H2)))
-H1)))))))))).
+b0) w0)))) (\lambda (x0: C).(\lambda (H5: (getl (S (plus h i)) c2 (CHead x0
+(Bind b0) w0))).(let H_y0 \def (getl_conf_le (S (plus h i)) (CHead x0 (Bind
+b0) w0) c2 H5 (CHead x (Bind b) w) i H2) in (let H6 \def (refl_equal nat
+(plus (S h) i)) in (let H7 \def (eq_ind nat (S (plus h i)) (\lambda (n:
+nat).(getl (minus n i) (CHead x (Bind b) w) (CHead x0 (Bind b0) w0))) (H_y0
+(le_S i (plus h i) (le_plus_r h i))) (plus (S h) i) H6) in (let H8 \def
+(eq_ind nat (minus (plus (S h) i) i) (\lambda (n: nat).(getl n (CHead x (Bind
+b) w) (CHead x0 (Bind b0) w0))) H7 (S h) (minus_plus_r (S h) i)) in (ex_intro
+C (\lambda (d2: C).(getl h x (CHead d2 (Bind b0) w0))) x0 (getl_gen_S (Bind
+b) x (CHead x0 (Bind b0) w0) w h H8)))))))) H4))))))))) H2))) H1)))))))))).