DEFINITION sty1_trans()
TYPE =
       ∀g:G.∀c:C.∀t1:T.∀t:T.(sty1 g c t1 t)→∀t2:T.(sty1 g c t t2)→(sty1 g c t1 t2)
BODY =
        assume g: G
        assume c: C
        assume t1: T
        assume t: T
        suppose H: sty1 g c t1 t
        assume t2: T
        suppose H0: sty1 g c t t2
          we proceed by induction on H0 to prove sty1 g c t1 t2
             case sty1_sty0 : t3:T H1:sty0 g c t t3 ⇒
                the thesis becomes sty1 g c t1 t3
                   by (sty1_sing . . . . H . H1)
sty1 g c t1 t3
             case sty1_sing : t0:T :sty1 g c t t0 t3:T H3:sty0 g c t0 t3 ⇒
                the thesis becomes sty1 g c t1 t3
                (H2) by induction hypothesis we know sty1 g c t1 t0
                   by (sty1_sing . . . . H2 . H3)
sty1 g c t1 t3
          we proved sty1 g c t1 t2
       we proved ∀g:G.∀c:C.∀t1:T.∀t:T.(sty1 g c t1 t)→∀t2:T.(sty1 g c t t2)→(sty1 g c t1 t2)