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