INDUCTIVE DEFINITION csubv () [ ]
OF ARITY C→C→Prop
BUILT FROM:
     csubv_sort: ∀n:nat.(csubv (CSort n) (CSort n))
   | csubv_void: ∀c1:C
                           .∀c2:C
                             .csubv c1 c2
                               →∀v1:T.∀v2:T.(csubv (CHead c1 (Bind Void) v1) (CHead c2 (Bind Void) v2))
   | csubv_bind: ∀c1:C
                           .∀c2:C
                             .csubv c1 c2
                               →∀b1:B
                                    .not (eq B b1 Void)
                                      →∀b2:B.∀v1:T.∀v2:T.(csubv (CHead c1 (Bind b1) v1) (CHead c2 (Bind b2) v2))
   | csubv_flat: ∀c1:C
                           .∀c2:C
                             .(csubv c1 c2)→∀f1:F.∀f2:F.∀v1:T.∀v2:T.(csubv (CHead c1 (Flat f1) v1) (CHead c2 (Flat f2) v2))