DEFINITION ty3_inv_appls_lref_nf2()
TYPE =
       ∀g:G
         .∀c:C
           .∀vs:TList
             .∀u1:T
               .∀i:nat
                 .ty3 g c (THeads (Flat Appl) vs (TLRef i)) u1
                   →(nf2 c (TLRef i)
                        →(nf2 c u1
                             →(ex2
                                  T
                                  λu:T.nf2 c (lift (S i) O u)
                                  λu:T.pc3 c (THeads (Flat Appl) vs (lift (S i) O u)) u1)))
BODY =
Show proof