INDUCTIVE DEFINITION csubc () [ :G ]
OF ARITY C→C→Prop
BUILT FROM:
     csubc_sort: ∀n:nat.(csubc g (CSort n) (CSort n))
   | csubc_head: ∀c1:C.∀c2:C.(csubc g c1 c2)→∀k:K.∀v:T.(csubc g (CHead c1 k v) (CHead c2 k v))
   | csubc_void: ∀c1:C
                           .∀c2:C
                             .csubc g c1 c2
                               →∀b:B
                                    .not (eq B b Void)
                                      →∀u1:T.∀u2:T.(csubc g (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2))
   | csubc_abst: ∀c1:C
                           .∀c2:C
                             .csubc g c1 c2
                               →∀v:T
                                    .∀a:A
                                      .sc3 g (asucc g a) c1 v
                                        →∀w:T
                                             .sc3 g a c2 w
                                               →csubc g (CHead c1 (Bind Abst) v) (CHead c2 (Bind Abbr) w)