DEFINITION csubc_getl_conf()
TYPE =
       ∀g:G
         .∀c1:C
           .∀e1:C
             .∀i:nat.(getl i c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2)
BODY =
        assume g: G
        assume c1: C
        assume e1: C
        assume i: nat
        suppose H: getl i c1 e1
        assume c2: C
        suppose H0: csubc g c1 c2
          (H1) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop i O c1 e λe:C.clear e e1
          end of H1
          we proceed by induction on H1 to prove ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
             case ex_intro2 : x:C H2:drop i O c1 x H3:clear x e1 ⇒
                the thesis becomes ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
                   (H_x) 
                      by (csubc_drop_conf_O . . . . H2 . H0)
ex2 C λe2:C.drop i O c2 e2 λe2:C.csubc g x e2
                   end of H_x
                   (H4) consider H_x
                   we proceed by induction on H4 to prove ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
                      case ex_intro2 : x0:C H5:drop i O c2 x0 H6:csubc g x x0 ⇒
                         the thesis becomes ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
                            (H_x0) 
                               by (csubc_clear_conf . . . H3 . H6)
ex2 C λe2:C.clear x0 e2 λe2:C.csubc g e1 e2
                            end of H_x0
                            (H7) consider H_x0
                            we proceed by induction on H7 to prove ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
                               case ex_intro2 : x1:C H8:clear x0 x1 H9:csubc g e1 x1 ⇒
                                  the thesis becomes ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
                                     by (getl_intro . . . . H5 H8)
                                     we proved getl i c2 x1
                                     by (ex_intro2 . . . . previous H9)
ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
          we proved ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2
       we proved 
          ∀g:G
            .∀c1:C
              .∀e1:C
                .∀i:nat.(getl i c1 e1)→∀c2:C.(csubc g c1 c2)→(ex2 C λe2:C.getl i c2 e2 λe2:C.csubc g e1 e2)