INDUCTIVE DEFINITION getl () [ :nat, :C, :C ]
OF ARITY Prop
BUILT FROM:
     getl_intro: ∀e:C.(drop h O c1 e)→(clear e c2)→(getl h c1 c2)