(k: K).(K_ind (\lambda (k0: K).(\forall (t: T).(csubv (CHead c0 k0 t) (CHead
c0 k0 t)))) (\lambda (b: B).(\lambda (t: T).(csubv_bind_same c0 c0 H b t t)))
(\lambda (f: F).(\lambda (t: T).(csubv_flat c0 c0 H f f t t))) k)))) c).
(k: K).(K_ind (\lambda (k0: K).(\forall (t: T).(csubv (CHead c0 k0 t) (CHead
c0 k0 t)))) (\lambda (b: B).(\lambda (t: T).(csubv_bind_same c0 c0 H b t t)))
(\lambda (f: F).(\lambda (t: T).(csubv_flat c0 c0 H f f t t))) k)))) c).