DEFINITION csubt_gen_flat()
TYPE =
       ∀g:G
         .∀e1:C
           .∀c2:C
             .∀v:T
               .∀f:F
                 .csubt g (CHead e1 (Flat f) v) c2
                   →ex2 C λe2:C.eq C c2 (CHead e2 (Flat f) v) λe2:C.csubt g e1 e2
BODY =
Show proof