DEFINITION ty3_inv_lref_nf2_pc3()
TYPE =
       ∀g:G
         .∀c:C
           .∀u1:T
             .∀i:nat
               .ty3 g c (TLRef i) u1
                 →(nf2 c (TLRef i)
                      →∀u2:T.(nf2 c u2)→(pc3 c u1 u2)→(ex T λu:T.eq T u2 (lift (S i) O u)))
BODY =
Show proof