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