DEFINITION arity_gen_cvoid()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀a:A
               .arity g c t a
                 →∀d:C
                      .∀u:T
                        .∀i:nat
                          .getl i c (CHead d (Bind Void) u)
                            →ex T λv:T.eq T t (lift (S O) i v)
BODY =
        assume g: G
        assume c: C
        assume t: T
        assume a: A
        suppose H: arity g c t a
        assume d: C
        assume u: T
        assume i: nat
        suppose H0: getl i c (CHead d (Bind Void) u)
          (H_x) 
             by (dnf_dec . . .)
ex T λv:T.or (subst0 i u t (lift (S O) i v)) (eq T t (lift (S O) i v))
          end of H_x
          (H1) consider H_x
          we proceed by induction on H1 to prove ex T λv:T.eq T t (lift (S O) i v)
             case ex_intro : x:T H2:or (subst0 i u t (lift (S O) i x)) (eq T t (lift (S O) i x)) ⇒
                the thesis becomes ex T λv:T.eq T t (lift (S O) i v)
                   we proceed by induction on H2 to prove ex T λv:T.eq T t (lift (S O) i v)
                      case or_introl : H3:subst0 i u t (lift (S O) i x) ⇒
                         the thesis becomes ex T λv:T.eq T t (lift (S O) i v)
                            by (arity_gen_cvoid_subst0 . . . . H . . . H0 . . H3 .)
ex T λv:T.eq T t (lift (S O) i v)
                      case or_intror : H3:eq T t (lift (S O) i x) ⇒
                         the thesis becomes ex T λv:T.eq T t (lift (S O) i v)
                            by (refl_equal . .)
                            we proved eq T (lift (S O) i x) (lift (S O) i x)
                            by (ex_intro . . . previous)
                            we proved ex T λv:T.eq T (lift (S O) i x) (lift (S O) i v)
                            by (eq_ind_r . . . previous . H3)
ex T λv:T.eq T t (lift (S O) i v)
ex T λv:T.eq T t (lift (S O) i v)
          we proved ex T λv:T.eq T t (lift (S O) i v)
       we proved 
          ∀g:G
            .∀c:C
              .∀t:T
                .∀a:A
                  .arity g c t a
                    →∀d:C
                         .∀u:T
                           .∀i:nat
                             .getl i c (CHead d (Bind Void) u)
                               →ex T λv:T.eq T t (lift (S O) i v)