INDUCTIVE DEFINITION sty1 () [ :G, :C, :T ]
OF ARITY T→Prop
BUILT FROM:
     sty1_sty0: ∀t2:T.(sty0 g c t1 t2)→(sty1 g c t1 t2)
   | sty1_sing: ∀t:T.(sty1 g c t1 t)→∀t2:T.(sty0 g c t t2)→(sty1 g c t1 t2)