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 =
        assume g: G
        assume b: B
        assume c: C
        assume v: T
        assume t1: T
        assume t2: T
        suppose H: sty1 g (CHead c (Bind b) v) t1 t2
          we proceed by induction on H to prove sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t2)
             case sty1_sty0 : t3:T H0:sty0 g (CHead c (Bind b) v) t1 t3 ⇒
                the thesis becomes sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t3)
                   by (sty0_bind . . . . . . H0)
                   we proved sty0 g c (THead (Bind b) v t1) (THead (Bind b) v t3)
                   by (sty1_sty0 . . . . previous)
sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t3)
             case sty1_sing : t:T :sty1 g (CHead c (Bind b) v) t1 t t3:T H2:sty0 g (CHead c (Bind b) v) t t3 ⇒
                the thesis becomes sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t3)
                (H1) by induction hypothesis we know sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t)
                   by (sty0_bind . . . . . . H2)
                   we proved sty0 g c (THead (Bind b) v t) (THead (Bind b) v t3)
                   by (sty1_sing . . . . H1 . previous)
sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t3)
          we proved sty1 g c (THead (Bind b) v t1) (THead (Bind b) v t2)
       we proved 
          ∀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)