DEFINITION sty1_bind()
TYPE =
       ∀g:G
         .∀b:B
           .∀c:C
             .∀v:T
               .∀t1:T
                 .∀t2:T
                   .sty1 g (CHead c (Bind b) v) t1 t2
                     →sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t2)
BODY =
Show proof