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 =
        assume k: K
        assume u: T
        assume t: T
        assume h: nat
        assume d: nat
          by (refl_equal . .)
          we proved 
             eq
               T
               THead k (lift h d u) (lift h (s k d) t)
               THead k (lift h d u) (lift h (s k d) t)
          that is equivalent to 
             eq
               T
               lift h d (THead k u t)
               THead k (lift h d u) (lift h (s k d) t)
       we proved 
          ∀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)