DEFINITION arity_nf2_inv_all()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀a:A
               .arity g c t a
                 →(nf2 c t
                      →(or3
                           ex3_2
                             T
                             T
                             λw:T.λu:T.eq T t (THead (Bind Abst) w u)
                             λw:T.λ:T.nf2 c w
                             λw:T.λu:T.nf2 (CHead c (Bind Abst) w) u
                           ex nat λn:nat.eq T t (TSort 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