DEFINITION csuba_gen_flat_rev()
TYPE =
       ∀g:G
         .∀d1:C
           .∀c:C
             .∀u1:T
               .∀f:F
                 .csuba g c (CHead d1 (Flat f) u1)
                   →ex2_2 C T λd2:C.λu2:T.eq C c (CHead d2 (Flat f) u2) λd2:C.λ:T.csuba g d2 d1
BODY =
Show proof