DEFINITION getl_gen_S()
TYPE =
       ∀k:K
         .∀c:C.∀x:C.∀u:T.∀h:nat.(getl (S h) (CHead c k u) x)→(getl (r k h) c x)
BODY =
        assume k: K
        assume c: C
        assume x: C
        assume u: T
        assume h: nat
        suppose H: getl (S h) (CHead c k u) x
          (H0) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop (S h) O (CHead c k u) e λe:C.clear e x
          end of H0
          we proceed by induction on H0 to prove getl (r k h) c x
             case ex_intro2 : x0:C H1:drop (S h) O (CHead c k u) x0 H2:clear x0 x ⇒
                the thesis becomes getl (r k h) c x
                   by (drop_gen_drop . . . . . H1)
                   we proved drop (r k h) O c x0
                   by (getl_intro . . . . previous H2)
getl (r k h) c x
          we proved getl (r k h) c x
       we proved 
          ∀k:K
            .∀c:C.∀x:C.∀u:T.∀h:nat.(getl (S h) (CHead c k u) x)→(getl (r k h) c x)