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 =
Show proof