INDUCTIVE DEFINITION sty0 () [ :G ]
OF ARITY C→T→T→Prop
BUILT FROM:
     sty0_sort: ∀c:C.∀n:nat.(sty0 g c (TSort n) (TSort (next g n)))
   | sty0_abbr: ∀c:C
                         .∀d:C
                           .∀v:T
                             .∀i:nat
                               .getl i c (CHead d (Bind Abbr) v)
                                 →∀w:T.(sty0 g d v w)→(sty0 g c (TLRef i) (lift (S i) O w))
   | sty0_abst: ∀c:C
                         .∀d:C
                           .∀v:T
                             .∀i:nat
                               .getl i c (CHead d (Bind Abst) v)
                                 →∀w:T.(sty0 g d v w)→(sty0 g c (TLRef i) (lift (S i) O v))
   | sty0_bind: ∀b:B
                         .∀c:C
                           .∀v:T
                             .∀t1:T
                               .∀t2:T
                                 .sty0 g (CHead c (Bind b) v) t1 t2
                                   →sty0 g c (THead (Bind b) v t1) (THead (Bind b) v t2)
   | sty0_appl: ∀c:C
                         .∀v:T
                           .∀t1:T
                             .∀t2:T
                               .(sty0 g c t1 t2)→(sty0 g c (THead (Flat Appl) v t1) (THead (Flat Appl) v t2))
   | sty0_cast: ∀c:C
                         .∀v1:T
                           .∀v2:T
                             .sty0 g c v1 v2
                               →∀t1:T.∀t2:T.(sty0 g c t1 t2)→(sty0 g c (THead (Flat Cast) v1 t1) (THead (Flat Cast) v2 t2))