DEFINITION thead_x_lift_y_y()
TYPE =
       ∀k:K.∀t:T.∀v:T.∀h:nat.∀d:nat.(eq T (THead k v (lift h d t)) t)→∀P:Prop.P
BODY =
Show proof