DEFINITION getl_gen_all()
TYPE =
       ∀c1:C.∀c2:C.∀i:nat.(getl i c1 c2)→(ex2 C λe:C.drop i O c1 e λe:C.clear e c2)
BODY =
        assume c1: C
        assume c2: C
        assume i: nat
        suppose H: getl i c1 c2
          we proceed by induction on H to prove ex2 C λe:C.drop i O c1 e λe:C.clear e c2
             case getl_intro : e:C H0:drop i O c1 e H1:clear e c2 ⇒
                the thesis becomes ex2 C λe0:C.drop i O c1 e0 λe0:C.clear e0 c2
                   by (ex_intro2 . . . . H0 H1)
ex2 C λe0:C.drop i O c1 e0 λe0:C.clear e0 c2
          we proved ex2 C λe:C.drop i O c1 e λe:C.clear e c2
       we proved ∀c1:C.∀c2:C.∀i:nat.(getl i c1 c2)→(ex2 C λe:C.drop i O c1 e λe:C.clear e c2)