DEFINITION lift_r()
TYPE =
       ∀t:T.∀d:nat.(eq T (lift O d t) t)
BODY =
       assume t: T
          we proceed by induction on t to prove ∀d:nat.(eq T (lift O d t) t)
             case TSort : n:nat ⇒
                the thesis becomes nat→(eq T (TSort n) (TSort n))
                   assume : nat
                      by (refl_equal . .)
                      we proved eq T (TSort n) (TSort n)
                      that is equivalent to eq T (lift O __1 (TSort n)) (TSort n)
nat→(eq T (TSort n) (TSort n))
             case TLRef : n:nat ⇒
                the thesis becomes ∀d:nat.(eq T (lift O d (TLRef n)) (TLRef n))
                   assume d: nat
                      (h1) 
                         suppose H: lt n d
                            (h1) 
                               by (refl_equal . .)
eq T (TLRef n) (TLRef n)
                            end of h1
                            (h2) 
                               by (lift_lref_lt . . . H)
eq T (lift O d (TLRef n)) (TLRef n)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved eq T (lift O d (TLRef n)) (TLRef n)
(lt n d)→(eq T (lift O d (TLRef n)) (TLRef n))
                      end of h1
                      (h2) 
                         suppose H: le d n
                            (h1) 
                               by (plus_n_O .)
                               we proved eq nat n (plus n O)
                               by (sym_eq . . . previous)
                               we proved eq nat (plus n O) n
                               by (f_equal . . . . . previous)
eq T (TLRef (plus n O)) (TLRef n)
                            end of h1
                            (h2) 
                               by (lift_lref_ge . . . H)
eq T (lift O d (TLRef n)) (TLRef (plus n O))
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved eq T (lift O d (TLRef n)) (TLRef n)
(le d n)→(eq T (lift O d (TLRef n)) (TLRef n))
                      end of h2
                      by (lt_le_e . . . h1 h2)
                      we proved eq T (lift O d (TLRef n)) (TLRef n)
∀d:nat.(eq T (lift O d (TLRef n)) (TLRef n))
             case THead : k:K t0:T t1:T ⇒
                the thesis becomes ∀d:nat.(eq T (lift O d (THead k t0 t1)) (THead k t0 t1))
                (H) by induction hypothesis we know ∀d:nat.(eq T (lift O d t0) t0)
                (H0) by induction hypothesis we know ∀d:nat.(eq T (lift O d t1) t1)
                   assume d: nat
                      (h1) 
                         (h1) 
                            by (refl_equal . .)
eq K k k
                         end of h1
                         (h2) 
                            by (H .)
eq T (lift O d t0) t0
                         end of h2
                         (h3) 
                            by (H0 .)
eq T (lift O (s k d) t1) t1
                         end of h3
                         by (f_equal3 . . . . . . . . . . . h1 h2 h3)
eq T (THead k (lift O d t0) (lift O (s k d) t1)) (THead k t0 t1)
                      end of h1
                      (h2) 
                         by (lift_head . . . . .)

                            eq
                              T
                              lift O d (THead k t0 t1)
                              THead k (lift O d t0) (lift O (s k d) t1)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved eq T (lift O d (THead k t0 t1)) (THead k t0 t1)
∀d:nat.(eq T (lift O d (THead k t0 t1)) (THead k t0 t1))
          we proved ∀d:nat.(eq T (lift O d t) t)
       we proved ∀t:T.∀d:nat.(eq T (lift O d t) t)