DEFINITION getl_ind()
TYPE =
       ∀h:nat
         .∀c1:C
           .∀c2:C
             .∀P:Prop
               .(∀c:C.(drop h O c1 c)→(clear c c2)→P)→(getl h c1 c2)→P
BODY =
        assume h: nat
        assume c1: C
        assume c2: C
        assume P: Prop
        suppose H: ∀c:C.(drop h O c1 c)→(clear c c2)→P
        suppose H1: getl h c1 c2
          by cases on H1 we prove P
             case getl_intro c:C H2:drop h O c1 c H3:clear c c2 ⇒
                the thesis becomes P
                by (H . H2 H3)
P
          we proved P
       we proved 
          ∀h:nat
            .∀c1:C
              .∀c2:C
                .∀P:Prop
                  .(∀c:C.(drop h O c1 c)→(clear c c2)→P)→(getl h c1 c2)→P