DEFINITION csuba_gen_bind_rev()
TYPE =
       ∀g:G
         .∀b1:B
           .∀e1:C
             .∀c2:C
               .∀v1:T
                 .csuba g c2 (CHead e1 (Bind b1) v1)
                   →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 e2 e1
BODY =
Show proof