DEFINITION thead_x_y_y()
TYPE =
       ∀k:K.∀v:T.∀t:T.(eq T (THead k v t) t)→∀P:Prop.P
BODY =
Show proof