DEFINITION subst_head()
TYPE =
       ∀k:K
         .∀w:T
           .∀u:T
             .∀t:T
               .∀d:nat
                 .eq
                   T
                   subst d w (THead k u t)
                   THead k (subst d w u) (subst (s k d) w t)
BODY =
        assume k: K
        assume w: T
        assume u: T
        assume t: T
        assume d: nat
          by (refl_equal . .)
          we proved 
             eq
               T
               THead k (subst d w u) (subst (s k d) w t)
               THead k (subst d w u) (subst (s k d) w t)
          that is equivalent to 
             eq
               T
               subst d w (THead k u t)
               THead k (subst d w u) (subst (s k d) w t)
       we proved 
          ∀k:K
            .∀w:T
              .∀u:T
                .∀t:T
                  .∀d:nat
                    .eq
                      T
                      subst d w (THead k u t)
                      THead k (subst d w u) (subst (s k d) w t)