C).(\lambda (H1: (drop i O c x)).(\lambda (H2: (clear x (CHead d (Bind b)
u))).(getl_intro i (CTail k v c) (CHead (CTail k v d) (Bind b) u) (CTail k v
x) (drop_ctail c x O i H1 k v) (clear_ctail b x d u H2 k v))))) H0))))))))).
C).(\lambda (H1: (drop i O c x)).(\lambda (H2: (clear x (CHead d (Bind b)
u))).(getl_intro i (CTail k v c) (CHead (CTail k v d) (Bind b) u) (CTail k v
x) (drop_ctail c x O i H1 k v) (clear_ctail b x d u H2 k v))))) H0))))))))).