DEFINITION sty1_ind()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀P:T→Prop
               .∀t:T.(sty0 g c t1 t)→(P t)
                 →(∀t:T.(sty1 g c t1 t)→(P t)→∀t2:T.(sty0 g c t t2)→(P t2)
                      →∀t:T.(sty1 g c t1 t)→(P t))
BODY =
Show proof