INDUCTIVE DEFINITION ty3 () [ :G ]
OF ARITY CTTProp
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))