DEFINITION ty3_nf2_inv_sort()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀m:nat
               .ty3 g c t (TSort m)
                 →(nf2 c t
                      →(or
                           ex2 nat λn:nat.eq T t (TSort n) λn:nat.eq nat m (next g n)
                           ex3_2
                             TList
                             nat
                             λws:TList.λi:nat.eq T t (THeads (Flat Appl) ws (TLRef i))
                             λws:TList.λ:nat.nfs2 c ws
                             λ:TList.λi:nat.nf2 c (TLRef i)))
BODY =
Show proof