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

                eq
                  T
                  <λb1:bool.T>
                    CASE true OF
                      true⇒TLRef i
                    | false⇒<λb1:bool.T> CASE blt d i OF true⇒TLRef (pred i) | false⇒lift d O v
                  TLRef i
          end of h1
          (h2) 
             by (lt_blt . . H)
eq bool (blt i d) true
          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 i
          that is equivalent to eq T (subst d v (TLRef i)) (TLRef i)
       we proved 
          ∀v:T
            .∀d:nat.∀i:nat.(lt i d)→(eq T (subst d v (TLRef i)) (TLRef i))