DEFINITION ty3_inv_lref_lref_nf2()
TYPE =
       ∀g:G
         .∀c:C
           .∀i:nat
             .∀j:nat
               .ty3 g c (TLRef i) (TLRef j)
                 →(nf2 c (TLRef i))→(nf2 c (TLRef j))→(lt i j)
BODY =
Show proof