DEFINITION ty3_gen_bind()
TYPE =
       ∀g:G
         .∀b:B
           .∀c:C
             .∀u:T
               .∀t1:T
                 .∀x:T
                   .ty3 g c (THead (Bind b) u t1) x
                     →(ex3_2
                          T
                          T
                          λt2:T.λ:T.pc3 c (THead (Bind b) u t2) x
                          λ:T.λt:T.ty3 g c u t
                          λt2:T.λ:T.ty3 g (CHead c (Bind b) u) t1 t2)
BODY =
Show proof