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 =
Show proof