DEFINITION getl_gen_O()
TYPE =
       ∀e:C.∀x:C.(getl O e x)→(clear e x)
BODY =
        assume e: C
        assume x: C
        suppose H: getl O e x
          (H0) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop O O e e λe:C.clear e x
          end of H0
          we proceed by induction on H0 to prove clear e x
             case ex_intro2 : x0:C H1:drop O O e x0 H2:clear x0 x ⇒
                the thesis becomes clear e x
                   (H3) 
                      by (drop_gen_refl . . H1)
                      we proved eq C e x0
                      by (eq_ind_r . . . H2 . previous)
clear e x
                   end of H3
                   consider H3
clear e x
          we proved clear e x
       we proved ∀e:C.∀x:C.(getl O e x)→(clear e x)