DEFINITION chead_ctail()
TYPE =
       ∀c:C.∀t:T.∀k:K.(ex_3 K C T λh:K.λd:C.λu:T.eq C (CHead c k t) (CTail h u d))
BODY =
Show proof