INDUCTIVE DEFINITION ty3 () [ :G ]
OF ARITY C→T→T→Prop
BUILT FROM:
     ty3_conv: ∀c:C.∀t2:T.∀t:T.(ty3 g c t2 t)→∀u:T.∀t1:T.(ty3 g c u t1)→(pc3 c t1 t2)→(ty3 g c u t2)
   | ty3_sort: ∀c:C.∀m:nat.(ty3 g c (TSort m) (TSort (next g m)))
   | ty3_abbr: ∀n:nat
                       .∀c:C
                         .∀d:C
                           .∀u:T
                             .getl n c (CHead d (Bind Abbr) u)
                               →∀t:T.(ty3 g d u t)→(ty3 g c (TLRef n) (lift (S n) O t))
   | ty3_abst: ∀n:nat
                       .∀c:C
                         .∀d:C
                           .∀u:T
                             .getl n c (CHead d (Bind Abst) u)
                               →∀t:T.(ty3 g d u t)→(ty3 g c (TLRef n) (lift (S n) O u))
   | ty3_bind: ∀c:C
                       .∀u:T
                         .∀t:T
                           .ty3 g c u t
                             →∀b:B
                                  .∀t1:T
                                    .∀t2:T
                                      .ty3 g (CHead c (Bind b) u) t1 t2
                                        →ty3 g c (THead (Bind b) u t1) (THead (Bind b) u t2)
   | ty3_appl: ∀c:C
                       .∀w:T
                         .∀u:T
                           .ty3 g c w u
                             →∀v:T
                                  .∀t:T
                                    .ty3 g c v (THead (Bind Abst) u t)
                                      →(ty3
                                           g
                                           c
                                           THead (Flat Appl) w v
                                           THead (Flat Appl) w (THead (Bind Abst) u t))
   | ty3_cast: ∀c:C
                       .∀t1:T
                         .∀t2:T
                           .ty3 g c t1 t2
                             →∀t0:T.(ty3 g c t2 t0)→(ty3 g c (THead (Flat Cast) t2 t1) (THead (Flat Cast) t0 t2))