DEFINITION getl_ctail()
TYPE =
       ∀b:B
         .∀c:C
           .∀d:C
             .∀u:T
               .∀i:nat
                 .getl i c (CHead d (Bind b) u)
                   →∀k:K.∀v:T.(getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u))
BODY =
        assume b: B
        assume c: C
        assume d: C
        assume u: T
        assume i: nat
        suppose H: getl i c (CHead d (Bind b) u)
        assume k: K
        assume v: T
          (H0) 
             by (getl_gen_all . . . H)
ex2 C λe:C.drop i O c e λe:C.clear e (CHead d (Bind b) u)
          end of H0
          we proceed by induction on H0 to prove getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)
             case ex_intro2 : x:C H1:drop i O c x H2:clear x (CHead d (Bind b) u) ⇒
                the thesis becomes getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)
                   (h1) 
                      by (drop_ctail . . . . H1 . .)
drop i O (CTail k v c) (CTail k v x)
                   end of h1
                   (h2) 
                      by (clear_ctail . . . . H2 . .)
clear (CTail k v x) (CHead (CTail k v d) (Bind b) u)
                   end of h2
                   by (getl_intro . . . . h1 h2)
getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)
          we proved getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)
       we proved 
          ∀b:B
            .∀c:C
              .∀d:C
                .∀u:T
                  .∀i:nat
                    .getl i c (CHead d (Bind b) u)
                      →∀k:K.∀v:T.(getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u))