DEFINITION csubv_getl_conf()
TYPE =
       ∀c1:C
         .∀c2:C
           .csubv c1 c2
             →∀b1:B
                  .∀d1:C
                    .∀v1:T
                      .∀i:nat
                        .getl i c1 (CHead d1 (Bind b1) v1)
                          →ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
BODY =
        assume c1: C
        assume c2: C
        suppose H: csubv c1 c2
        assume b1: B
        assume d1: C
        assume v1: T
        assume i: nat
        suppose H0: getl i c1 (CHead d1 (Bind b1) v1)
          (H1) 
             by (getl_gen_all . . . H0)
ex2 C λe:C.drop i O c1 e λe:C.clear e (CHead d1 (Bind b1) v1)
          end of H1
          we proceed by induction on H1 to prove ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
             case ex_intro2 : x:C H2:drop i O c1 x H3:clear x (CHead d1 (Bind b1) v1) ⇒
                the thesis becomes ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) 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_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
                      case ex_intro2 : x0:C H5:csubv x x0 H6:drop i O c2 x0 ⇒
                         the thesis becomes ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
                            (H_x0) 
                               by (csubv_clear_conf . . H5 . . . H3)
ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.clear x0 (CHead d2 (Bind b2) v2)
                            end of H_x0
                            (H7) consider H_x0
                            we proceed by induction on H7 to prove ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
                               case ex2_3_intro : x1:B x2:C x3:T H8:csubv d1 x2 H9:clear x0 (CHead x2 (Bind x1) x3) ⇒
                                  the thesis becomes ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
                                     by (getl_intro . . . . H6 H9)
                                     we proved getl i c2 (CHead x2 (Bind x1) x3)
                                     by (ex2_3_intro . . . . . . . . H8 previous)
ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
          we proved ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)
       we proved 
          ∀c1:C
            .∀c2:C
              .csubv c1 c2
                →∀b1:B
                     .∀d1:C
                       .∀v1:T
                         .∀i:nat
                           .getl i c1 (CHead d1 (Bind b1) v1)
                             →ex2_3 B C T λ:B.λd2:C.λ:T.csubv d1 d2 λb2:B.λd2:C.λv2:T.getl i c2 (CHead d2 (Bind b2) v2)