DEFINITION lift_lref_gt()
TYPE =
       ∀d:nat
         .∀n:nat
           .lt d n
             →eq T (lift (S O) d (TLRef (pred n))) (TLRef n)
BODY =
        assume d: nat
        assume n: nat
        suppose H: lt d n
          (h1) 
             by (plus_sym . .)
             we proved eq nat (plus (S O) (pred n)) (plus (pred n) (S O))
             we proceed by induction on the previous result to prove eq T (TLRef (plus (pred n) (S O))) (TLRef n)
                case refl_equal : ⇒
                   the thesis becomes eq T (TLRef (plus (S O) (pred n))) (TLRef n)
                      by (S_pred . . H)
                      we proved eq nat n (S (pred n))
                      we proceed by induction on the previous result to prove eq T (TLRef (S (pred n))) (TLRef n)
                         case refl_equal : ⇒
                            the thesis becomes eq T (TLRef n) (TLRef n)
                               by (refl_equal . .)
eq T (TLRef n) (TLRef n)
                      we proved eq T (TLRef (S (pred n))) (TLRef n)
eq T (TLRef (plus (S O) (pred n))) (TLRef n)
eq T (TLRef (plus (pred n) (S O))) (TLRef n)
          end of h1
          (h2) 
             by (S_pred . . H)
             we proved eq nat n (S (pred n))
             we proceed by induction on the previous result to prove le (S d) (S (pred n))
                case refl_equal : ⇒
                   the thesis becomes le (S d) n
                      consider H
                      we proved lt d n
le (S d) n
             we proved le (S d) (S (pred n))
             by (le_S_n . . previous)
             we proved le d (pred n)
             by (lift_lref_ge . . . previous)

                eq
                  T
                  lift (S O) d (TLRef (pred n))
                  TLRef (plus (pred n) (S O))
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq T (lift (S O) d (TLRef (pred n))) (TLRef n)
       we proved 
          ∀d:nat
            .∀n:nat
              .lt d n
                →eq T (lift (S O) d (TLRef (pred n))) (TLRef n)