DEFINITION csubv_getl_conf_void()
TYPE =
       ∀c1:C
         .∀c2:C
           .csubv c1 c2
             →∀d1:C
                  .∀v1:T
                    .∀i:nat
                      .getl i c1 (CHead d1 (Bind Void) v1)
                        →ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
BODY =
        assume c1: C
        assume c2: C
        suppose H: csubv c1 c2
        assume d1: C
        assume v1: T
        assume i: nat
        suppose H0: getl i c1 (CHead d1 (Bind Void) v1)
          (H1) 
             by (getl_gen_all . . . H0)
ex2 C λe:C.drop i O c1 e λe:C.clear e (CHead d1 (Bind Void) v1)
          end of H1
          we proceed by induction on H1 to prove ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
             case ex_intro2 : x:C H2:drop i O c1 x H3:clear x (CHead d1 (Bind Void) v1) ⇒
                the thesis becomes ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
                   (H_x) 
                      by (csubv_drop_conf . . H . . H2)
ex2 C λe2:C.csubv x e2 λe2:C.drop i O c2 e2
                   end of H_x
                   (H4) consider H_x
                   we proceed by induction on H4 to prove ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
                      case ex_intro2 : x0:C H5:csubv x x0 H6:drop i O c2 x0 ⇒
                         the thesis becomes ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
                            (H_x0) 
                               by (csubv_clear_conf_void . . H5 . . H3)
ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.clear x0 (CHead d2 (Bind Void) v2)
                            end of H_x0
                            (H7) consider H_x0
                            we proceed by induction on H7 to prove ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
                               case ex2_2_intro : x1:C x2:T H8:csubv d1 x1 H9:clear x0 (CHead x1 (Bind Void) x2) ⇒
                                  the thesis becomes ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
                                     by (getl_intro . . . . H6 H9)
                                     we proved getl i c2 (CHead x1 (Bind Void) x2)
                                     by (ex2_2_intro . . . . . . H8 previous)
ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
          we proved ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)
       we proved 
          ∀c1:C
            .∀c2:C
              .csubv c1 c2
                →∀d1:C
                     .∀v1:T
                       .∀i:nat
                         .getl i c1 (CHead d1 (Bind Void) v1)
                           →ex2_2 C T λd2:C.λ:T.csubv d1 d2 λd2:C.λv2:T.getl i c2 (CHead d2 (Bind Void) v2)