DEFINITION lift_head()
TYPE =
       ∀k:K
         .∀u:T
           .∀t:T
             .∀h:nat
               .∀d:nat
                 .eq
                   T
                   lift h d (THead k u t)
                   THead k (lift h d u) (lift h (s k d) t)
BODY =
Show proof