DEFINITION ty3_nf2_inv_all()
TYPE =
       ∀g:G
         .∀c:C
           .∀t:T
             .∀u:T
               .ty3 g c t u
                 →(nf2 c t
                      →(or3
                           ex3_2
                             T
                             T
                             λw:T.λu0:T.eq T t (THead (Bind Abst) w u0)
                             λw:T.λ:T.nf2 c w
                             λw:T.λu0:T.nf2 (CHead c (Bind Abst) w) u0
                           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 =
        assume g: G
        assume c: C
        assume t: T
        assume u: T
        suppose H: ty3 g c t u
        suppose H0: nf2 c t
          (H_x) 
             by (ty3_arity . . . . H)
ex2 A λa1:A.arity g c t a1 λa1:A.arity g c u (asucc g a1)
          end of H_x
          (H1) consider H_x
          we proceed by induction on H1 to prove 
             or3
               ex3_2
                 T
                 T
                 λw:T.λu0:T.eq T t (THead (Bind Abst) w u0)
                 λw:T.λ:T.nf2 c w
                 λw:T.λu0:T.nf2 (CHead c (Bind Abst) w) u0
               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)
             case ex_intro2 : x:A H2:arity g c t x :arity g c u (asucc g x) ⇒
                the thesis becomes 
                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)
                   by (arity_nf2_inv_all . . . . H2 H0)

                      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)
          we proved 
             or3
               ex3_2
                 T
                 T
                 λw:T.λu0:T.eq T t (THead (Bind Abst) w u0)
                 λw:T.λ:T.nf2 c w
                 λw:T.λu0:T.nf2 (CHead c (Bind Abst) w) u0
               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)
       we proved 
          ∀g:G
            .∀c:C
              .∀t:T
                .∀u:T
                  .ty3 g c t u
                    →(nf2 c t
                         →(or3
                              ex3_2
                                T
                                T
                                λw:T.λu0:T.eq T t (THead (Bind Abst) w u0)
                                λw:T.λ:T.nf2 c w
                                λw:T.λu0:T.nf2 (CHead c (Bind Abst) w) u0
                              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)))