DEFINITION subst_lref_eq()
TYPE =
       ∀v:T.∀i:nat.(eq T (subst i v (TLRef i)) (lift i O v))
BODY =
        assume v: T
        assume i: nat
          (h1) 
             by (refl_equal . .)
             we proved eq T (lift i O v) (lift i O v)

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