DEFINITION flt_thead_sx()
TYPE =
∀
k:
K
.
∀
c:
C
.
∀
u:
T
.
∀
t:
T
.(
flt
c u c (
THead
k u t))
BODY =
Show proof