DEFINITION sty0_gen_bind()
TYPE =
       ∀g:G
         .∀b:B
           .∀c:C
             .∀u:T
               .∀t1:T
                 .∀x:T
                   .sty0 g c (THead (Bind b) u t1) x
                     →ex2 T λt2:T.sty0 g (CHead c (Bind b) u) t1 t2 λt2:T.eq T x (THead (Bind b) u t2)
BODY =
Show proof