DEFINITION clear_ctail()
TYPE =
       ∀b:B
         .∀c1:C
           .∀c2:C
             .∀u2:T
               .clear c1 (CHead c2 (Bind b) u2)
                 →∀k:K.∀u1:T.(clear (CTail k u1 c1) (CHead (CTail k u1 c2) (Bind b) u2))
BODY =
Show proof