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