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