INDUCTIVE DEFINITION arity () [ :G ]
OF ARITY C→T→A→Prop
BUILT FROM:
     arity_sort: ∀c:C.∀n:nat.(arity g c (TSort n) (ASort O n))
   | arity_abbr: ∀c:C
                           .∀d:C
                             .∀u:T
                               .∀i:nat
                                 .getl i c (CHead d (Bind Abbr) u)
                                   →∀a:A.(arity g d u a)→(arity g c (TLRef i) a)
   | arity_abst: ∀c:C
                           .∀d:C
                             .∀u:T
                               .∀i:nat
                                 .getl i c (CHead d (Bind Abst) u)
                                   →∀a:A.(arity g d u (asucc g a))→(arity g c (TLRef i) a)
   | arity_bind: ∀b:B
                           .not (eq B b Abst)
                             →∀c:C
                                  .∀u:T
                                    .∀a1:A
                                      .arity g c u a1
                                        →∀t:T
                                             .∀a2:A
                                               .arity g (CHead c (Bind b) u) t a2
                                                 →arity g c (THead (Bind b) u t) a2
   | arity_head: ∀c:C
                           .∀u:T
                             .∀a1:A
                               .arity g c u (asucc g a1)
                                 →∀t:T
                                      .∀a2:A
                                        .arity g (CHead c (Bind Abst) u) t a2
                                          →arity g c (THead (Bind Abst) u t) (AHead a1 a2)
   | arity_appl: ∀c:C
                           .∀u:T
                             .∀a1:A
                               .arity g c u a1
                                 →∀t:T
                                      .∀a2:A
                                        .(arity g c t (AHead a1 a2))→(arity g c (THead (Flat Appl) u t) a2)
   | arity_cast: ∀c:C
                           .∀u:T
                             .∀a:A
                               .arity g c u (asucc g a)
                                 →∀t:T.(arity g c t a)→(arity g c (THead (Flat Cast) u t) a)
   | arity_repl: ∀c:C.∀t:T.∀a1:A.(arity g c t a1)→∀a2:A.(leq g a1 a2)→(arity g c t a2)