DEFINITION subst_lref_gt()
TYPE =
       ∀v:T
         .∀d:nat
           .∀i:nat
             .(lt d i)→(eq T (subst d v (TLRef i)) (TLRef (pred i)))
BODY =
        assume v: T
        assume d: nat
        assume i: nat
        suppose H: lt d i
          (h1) 
             (h1) 
                by (refl_equal . .)
                we proved eq T (TLRef (pred i)) (TLRef (pred i))

                   eq
                     T
                     <λb1:bool.T> CASE true OF true⇒TLRef (pred i) | false⇒lift d O v
                     TLRef (pred i)
             end of h1
             (h2) 
                by (lt_blt . . H)
eq bool (blt d i) true
             end of h2
             by (eq_ind_r . . . h1 . h2)
             we proved 
                eq
                  T
                  <λb1:bool.T> CASE blt d i OF true⇒TLRef (pred i) | false⇒lift d O v
                  TLRef (pred i)

                eq
                  T
                  <λb1:bool.T>
                    CASE false OF
                      true⇒TLRef i
                    | false⇒<λb1:bool.T> CASE blt d i OF true⇒TLRef (pred i) | false⇒lift d O v
                  TLRef (pred i)
          end of h1
          (h2) 
             by (lt_le_weak . . H)
             we proved le d i
             by (le_bge . . previous)
eq bool (blt i d) false
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved 
             eq
               T
               <λb1:bool.T>
                 CASE blt i d OF
                   true⇒TLRef i
                 | false⇒<λb1:bool.T> CASE blt d i OF true⇒TLRef (pred i) | false⇒lift d O v
               TLRef (pred i)
          that is equivalent to eq T (subst d v (TLRef i)) (TLRef (pred i))
       we proved 
          ∀v:T
            .∀d:nat
              .∀i:nat
                .(lt d i)→(eq T (subst d v (TLRef i)) (TLRef (pred i)))