INDUCTIVE DEFINITION csubt () [ :G ]
OF ARITY C→C→Prop
BUILT FROM:
     csubt_sort: ∀n:nat.(csubt g (CSort n) (CSort n))
   | csubt_head: ∀c1:C.∀c2:C.(csubt g c1 c2)→∀k:K.∀u:T.(csubt g (CHead c1 k u) (CHead c2 k u))
   | csubt_void: ∀c1:C
                           .∀c2:C
                             .csubt g c1 c2
                               →∀b:B
                                    .not (eq B b Void)
                                      →∀u1:T.∀u2:T.(csubt g (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2))
   | csubt_abst: ∀c1:C
                           .∀c2:C
                             .csubt g c1 c2
                               →∀u:T
                                    .∀t:T
                                      .ty3 g c1 u t
                                        →(ty3 g c2 u t
                                             →csubt g (CHead c1 (Bind Abst) t) (CHead c2 (Bind Abbr) u))