DEFINITION theads_tapp()
TYPE =
       ∀k:K
         .∀v:T
           .∀t:T
             .∀vs:TList
               .eq T (THeads k (TApp vs v) t) (THeads k vs (THead k v t))
BODY =
Show proof