DEFINITION pr3_gen_lref()
TYPE =
       ∀c:C
         .∀x:T
           .∀n:nat
             .pr3 c (TLRef n) x
               →(or
                    eq T x (TLRef n)
                    ex3_3
                      C
                      T
                      T
                      λd:C.λu:T.λ:T.getl n c (CHead d (Bind Abbr) u)
                      λd:C.λu:T.λv:T.pr3 d u v
                      λ:C.λ:T.λv:T.eq T x (lift (S n) O v))
BODY =
Show proof