DEFINITION arity_ind()
TYPE =
       ∀g:G
         .∀P:C→T→A→Prop
           .∀c:C.∀n:nat.(P c (TSort n) (ASort O n))
             →(∀c:C
                    .∀c1:C
                      .∀t:T
                        .∀n:nat
                          .getl n c (CHead c1 (Bind Abbr) t)
                            →∀a:A.(arity g c1 t a)→(P c1 t a)→(P c (TLRef n) a)
                  →(∀c:C
                         .∀c1:C
                           .∀t:T
                             .∀n:nat
                               .getl n c (CHead c1 (Bind Abst) t)
                                 →∀a:A
                                      .arity g c1 t (asucc g a)
                                        →(P c1 t (asucc g a))→(P c (TLRef n) a)
                       →(∀b:B
                              .not (eq B b Abst)
                                →∀c:C
                                     .∀t:T
                                       .∀a:A
                                         .arity g c t a
                                           →(P c t a
                                                →∀t1:T
                                                     .∀a1:A
                                                       .arity g (CHead c (Bind b) t) t1 a1
                                                         →(P (CHead c (Bind b) t) t1 a1)→(P c (THead (Bind b) t t1) a1))
                            →(∀c:C
                                   .∀t:T
                                     .∀a:A
                                       .arity g c t (asucc g a)
                                         →(P c t (asucc g a)
                                              →∀t1:T
                                                   .∀a1:A
                                                     .arity g (CHead c (Bind Abst) t) t1 a1
                                                       →(P (CHead c (Bind Abst) t) t1 a1
                                                            →P c (THead (Bind Abst) t t1) (AHead a a1)))
                                 →(∀c:C
                                        .∀t:T
                                          .∀a:A
                                            .arity g c t a
                                              →(P c t a
                                                   →∀t1:T
                                                        .∀a1:A
                                                          .arity g c t1 (AHead a a1)
                                                            →(P c t1 (AHead a a1))→(P c (THead (Flat Appl) t t1) a1))
                                      →(∀c:C
                                             .∀t:T
                                               .∀a:A
                                                 .arity g c t (asucc g a)
                                                   →(P c t (asucc g a)
                                                        →∀t1:T.(arity g c t1 a)→(P c t1 a)→(P c (THead (Flat Cast) t t1) a))
                                           →(∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a)→∀a1:A.(leq g a a1)→(P c t a1)
                                                →∀c:C.∀t:T.∀a:A.(arity g c t a)→(P c t a))))))))
BODY =
Show proof