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 =
Show proof