INDUCTIVE DEFINITION csuba () [ :G ]
OF ARITY C→C→Prop
BUILT FROM:
     csuba_sort: ∀n:nat.(csuba g (CSort n) (CSort n))
   | csuba_head: ∀c1:C.∀c2:C.(csuba g c1 c2)→∀k:K.∀u:T.(csuba g (CHead c1 k u) (CHead c2 k u))
   | csuba_void: ∀c1:C
                           .∀c2:C
                             .csuba g c1 c2
                               →∀b:B
                                    .not (eq B b Void)
                                      →∀u1:T.∀u2:T.(csuba g (CHead c1 (Bind Void) u1) (CHead c2 (Bind b) u2))
   | csuba_abst: ∀c1:C
                           .∀c2:C
                             .csuba g c1 c2
                               →∀t:T
                                    .∀a:A
                                      .arity g c1 t (asucc g a)
                                        →∀u:T
                                             .arity g c2 u a
                                               →csuba g (CHead c1 (Bind Abst) t) (CHead c2 (Bind Abbr) u)