DEFINITION csuba_gen_bind()
TYPE =
       ∀g:G
         .∀b1:B
           .∀e1:C
             .∀c2:C
               .∀v1:T
                 .csuba g (CHead e1 (Bind b1) v1) c2
                   →ex2_3 B C T λb2:B.λe2:C.λv2:T.eq C c2 (CHead e2 (Bind b2) v2) λ:B.λe2:C.λ:T.csuba g e1 e2
BODY =
Show proof