DEFINITION cnt_lift()
TYPE =
       ∀t:T.(cnt t)→∀i:nat.∀d:nat.(cnt (lift i d t))
BODY =
        assume t: T
        suppose H: cnt t
          we proceed by induction on H to prove ∀i:nat.∀d:nat.(cnt (lift i d t))
             case cnt_sort : n:nat ⇒
                the thesis becomes ∀i:nat.∀d:nat.(cnt (lift i d (TSort n)))
                    assume i: nat
                    assume d: nat
                      (h1) 
                         by (cnt_sort .)
cnt (TSort n)
                      end of h1
                      (h2) 
                         by (lift_sort . . .)
eq T (lift i d (TSort n)) (TSort n)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved cnt (lift i d (TSort n))
∀i:nat.∀d:nat.(cnt (lift i d (TSort n)))
             case cnt_head : t0:T :cnt t0 k:K v:T ⇒
                the thesis becomes ∀i:nat.∀d:nat.(cnt (lift i d (THead k v t0)))
                (H1) by induction hypothesis we know ∀i:nat.∀d:nat.(cnt (lift i d t0))
                    assume i: nat
                    assume d: nat
                      (h1) 
                         by (H1 . .)
                         we proved cnt (lift i (s k d) t0)
                         by (cnt_head . previous . .)
cnt (THead k (lift i d v) (lift i (s k d) t0))
                      end of h1
                      (h2) 
                         by (lift_head . . . . .)

                            eq
                              T
                              lift i d (THead k v t0)
                              THead k (lift i d v) (lift i (s k d) t0)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved cnt (lift i d (THead k v t0))
∀i:nat.∀d:nat.(cnt (lift i d (THead k v t0)))
          we proved ∀i:nat.∀d:nat.(cnt (lift i d t))
       we proved ∀t:T.(cnt t)→∀i:nat.∀d:nat.(cnt (lift i d t))