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