H6) H7)))) H5))))) (\lambda (f: F).(\lambda (_: (getl (S n) (CHead c (Flat f)
t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f) t))).(clear_gen_flat_r f c1
c t H4 (getl (S n) c1 c3))))) k H1 H2))))))))) c2)))) i).
H6) H7)))) H5))))) (\lambda (f: F).(\lambda (_: (getl (S n) (CHead c (Flat f)
t) c3)).(\lambda (H4: (clear c1 (CHead c (Flat f) t))).(clear_gen_flat_r f c1
c t H4 (getl (S n) c1 c3))))) k H1 H2))))))))) c2)))) i).
x0) x2) H5) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: C).(getl i c1
c)) (getl_intro i c1 (CHead x1 (Bind x0) x2) x H2 H6) c3 (clear_gen_bind x0
x1 c3 x2 H7)))))))) H4))))) H1))))))).
x0) x2) H5) in (eq_ind_r C (CHead x1 (Bind x0) x2) (\lambda (c: C).(getl i c1
c)) (getl_intro i c1 (CHead x1 (Bind x0) x2) x H2 H6) c3 (clear_gen_bind x0
x1 c3 x2 H7)))))))) H4))))) H1))))))).
(CHead c0 (Flat f) t) (CHead e1 (Bind b) v))).(getl_flat c0 e2 (S n) (H e1 v
(clear_gen_flat f c0 (CHead e1 (Bind b) v) t H2) e2 n H1) f t))) k
H0))))))))))) c)).
(CHead c0 (Flat f) t) (CHead e1 (Bind b) v))).(getl_flat c0 e2 (S n) (H e1 v
(clear_gen_flat f c0 (CHead e1 (Bind b) v) t H2) e2 n H1) f t))) k
H0))))))))))) c)).
(\lambda (f: F).(\lambda (H3: (getl (S n) (CHead c (Flat f) t) c3)).(\lambda
(H4: (clear (CHead c (Flat f) t) c2)).(H0 c3 (getl_gen_S (Flat f) c c3 t n
H3) c2 (clear_gen_flat f c c2 t H4))))) k H1 H2))))))))) c1)))) i).
(\lambda (f: F).(\lambda (H3: (getl (S n) (CHead c (Flat f) t) c3)).(\lambda
(H4: (clear (CHead c (Flat f) t) c2)).(H0 c3 (getl_gen_S (Flat f) c c3 t n
H3) c2 (clear_gen_flat f c c2 t H4))))) k H1 H2))))))))) c1)))) i).