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 =
        assume k: K
        assume v: T
        assume t: T
        assume vs: TList
          we proceed by induction on vs to prove eq T (THeads k (TApp vs v) t) (THeads k vs (THead k v t))
             case TNil : ⇒
                the thesis becomes eq T (THeads k (TApp TNil v) t) (THeads k TNil (THead k v t))
                   by (refl_equal . .)
                   we proved eq T (THead k v t) (THead k v t)
eq T (THeads k (TApp TNil v) t) (THeads k TNil (THead k v t))
             case TCons : t0:T t1:TList ⇒
                the thesis becomes 
                eq
                  T
                  THeads k (TApp (TCons t0 t1) v) t
                  THeads k (TCons t0 t1) (THead k v t)
                (H) by induction hypothesis we know eq T (THeads k (TApp t1 v) t) (THeads k t1 (THead k v t))
                   we proceed by induction on H to prove 
                      eq
                        T
                        THead k t0 (THeads k (TApp t1 v) t)
                        THead k t0 (THeads k t1 (THead k v t))
                      case refl_equal : ⇒
                         the thesis becomes 
                         eq
                           T
                           THead k t0 (THeads k (TApp t1 v) t)
                           THead k t0 (THeads k (TApp t1 v) t)
                            by (refl_equal . .)

                               eq
                                 T
                                 THead k t0 (THeads k (TApp t1 v) t)
                                 THead k t0 (THeads k (TApp t1 v) t)
                   we proved 
                      eq
                        T
                        THead k t0 (THeads k (TApp t1 v) t)
                        THead k t0 (THeads k t1 (THead k v t))

                      eq
                        T
                        THeads k (TApp (TCons t0 t1) v) t
                        THeads k (TCons t0 t1) (THead k v t)
          we proved eq T (THeads k (TApp vs v) t) (THeads k vs (THead k v t))
       we proved 
          ∀k:K
            .∀v:T
              .∀t:T
                .∀vs:TList
                  .eq T (THeads k (TApp vs v) t) (THeads k vs (THead k v t))