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