DEFINITION ty3_inv_lref_nf2()
TYPE =
       ∀g:G
         .∀c:C
           .∀u:T
             .∀i:nat
               .ty3 g c (TLRef i) u
                 →(nf2 c (TLRef i))→(nf2 c u)→(ex T λu0:T.eq T u (lift (S i) O u0))
BODY =
        assume g: G
        assume c: C
        assume u: T
        assume i: nat
        suppose H: ty3 g c (TLRef i) u
        suppose H0: nf2 c (TLRef i)
        suppose H1: nf2 c u
          by (pc3_refl . .)
          we proved pc3 c u u
          by (ty3_inv_lref_nf2_pc3 . . . . H H0 . H1 previous)
          we proved ex T λu:T.eq T u (lift (S i) O u)
       we proved 
          ∀g:G
            .∀c:C
              .∀u:T
                .∀i:nat
                  .ty3 g c (TLRef i) u
                    →(nf2 c (TLRef i)
                         →(nf2 c u)→(ex T λu:T.eq T u (lift (S i) O u)))