DEFINITION tlt_head_sx()
TYPE =
∀
k:
K
.
∀
u:
T
.
∀
t:
T
.(
tlt
u (
THead
k u t))
BODY =
Show proof