DEFINITION clt_thead()
TYPE =
∀
k:
K
.
∀
u:
T
.
∀
c:
C
.(
clt
c (
CTail
k u c))
BODY =
Show proof