DEFINITION csuba_gen_void()
TYPE =
       ∀g:G
         .∀d1:C
           .∀c:C
             .∀u1:T
               .csuba g (CHead d1 (Bind Void) u1) c
                 →ex2_3 B C T λb:B.λd2:C.λu2:T.eq C c (CHead d2 (Bind b) u2) λ:B.λd2:C.λ:T.csuba g d1 d2
BODY =
Show proof