DEFINITION nf2_appl_lref()
TYPE =
       ∀c:C
         .∀u:T
           .nf2 c u
             →∀i:nat.(nf2 c (TLRef i))→(nf2 c (THead (Flat Appl) u (TLRef i)))
BODY =
        assume c: C
        assume u: T
        suppose H: nf2 c u
        assume i: nat
        suppose H0: nf2 c (TLRef i)
          (H_y) 
             by (nf2_appls_lref . . H0 .)

                nfs2 c (TCons u TNil)
                  →nf2 c (THeads (Flat Appl) (TCons u TNil) (TLRef i))
          end of H_y
          by (conj . . H I)
          we proved land (nf2 c u) True
          that is equivalent to nfs2 c (TCons u TNil)
          by (H_y previous)
          we proved nf2 c (THeads (Flat Appl) (TCons u TNil) (TLRef i))
          that is equivalent to nf2 c (THead (Flat Appl) u (TLRef i))
       we proved 
          ∀c:C
            .∀u:T
              .nf2 c u
                →∀i:nat.(nf2 c (TLRef i))→(nf2 c (THead (Flat Appl) u (TLRef i)))