c (Bind b) t) c3)) (clear_bind b c t) c2 (clear_gen_bind b c c2 t H3)))))
(\lambda (f: F).(\lambda (H2: (clear (CHead c (Flat f) t) c0)).(clear_flat c
c2 (H c0 (clear_gen_flat f c c0 t H2) c2 H1) f t))) k H0))))))))) c1).
c (Bind b) t) c3)) (clear_bind b c t) c2 (clear_gen_bind b c c2 t H3)))))
(\lambda (f: F).(\lambda (H2: (clear (CHead c (Flat f) t) c0)).(clear_flat c
c2 (H c0 (clear_gen_flat f c c0 t H2) c2 H1) f t))) k H0))))))))) c1).