DEFINITION nfs2_tapp()
TYPE =
       ∀c:C.∀t:T.∀ts:TList.(nfs2 c (TApp ts t))→(land (nfs2 c ts) (nf2 c t))
BODY =
        assume c: C
        assume t: T
        assume ts: TList
          we proceed by induction on ts to prove (nfs2 c (TApp ts t))→(land (nfs2 c ts) (nf2 c t))
             case TNil : ⇒
                the thesis becomes (nfs2 c (TApp TNil t))→(land (nfs2 c TNil) (nf2 c t))
                   we must prove (nfs2 c (TApp TNil t))→(land (nfs2 c TNil) (nf2 c t))
                   or equivalently (land (nf2 c t) True)→(land (nfs2 c TNil) (nf2 c t))
                   suppose H: land (nf2 c t) True
                      (H0) consider H
                      we proceed by induction on H0 to prove land True (nf2 c t)
                         case conj : H1:nf2 c t :True ⇒
                            the thesis becomes land True (nf2 c t)
                               by (conj . . I H1)
land True (nf2 c t)
                      we proved land True (nf2 c t)
                      that is equivalent to land (nfs2 c TNil) (nf2 c t)
                   we proved (land (nf2 c t) True)→(land (nfs2 c TNil) (nf2 c t))
(nfs2 c (TApp TNil t))→(land (nfs2 c TNil) (nf2 c t))
             case TCons : t0:T t1:TList ⇒
                the thesis becomes (nfs2 c (TApp (TCons t0 t1) t))→(land (nfs2 c (TCons t0 t1)) (nf2 c t))
                (H) by induction hypothesis we know (nfs2 c (TApp t1 t))→(land (nfs2 c t1) (nf2 c t))
                   we must prove (nfs2 c (TApp (TCons t0 t1) t))→(land (nfs2 c (TCons t0 t1)) (nf2 c t))
                   or equivalently (land (nf2 c t0) (nfs2 c (TApp t1 t)))→(land (nfs2 c (TCons t0 t1)) (nf2 c t))
                   suppose H0: land (nf2 c t0) (nfs2 c (TApp t1 t))
                      (H1) consider H0
                      we proceed by induction on H1 to prove land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)
                         case conj : H2:nf2 c t0 H3:nfs2 c (TApp t1 t) ⇒
                            the thesis becomes land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)
                               (H_x) 
                                  by (H H3)
land (nfs2 c t1) (nf2 c t)
                               end of H_x
                               (H4) consider H_x
                               we proceed by induction on H4 to prove land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)
                                  case conj : H5:nfs2 c t1 H6:nf2 c t ⇒
                                     the thesis becomes land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)
                                        by (conj . . H2 H5)
                                        we proved land (nf2 c t0) (nfs2 c t1)
                                        by (conj . . previous H6)
land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)
land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)
                      we proved land (land (nf2 c t0) (nfs2 c t1)) (nf2 c t)
                      that is equivalent to land (nfs2 c (TCons t0 t1)) (nf2 c t)
                   we proved (land (nf2 c t0) (nfs2 c (TApp t1 t)))→(land (nfs2 c (TCons t0 t1)) (nf2 c t))
(nfs2 c (TApp (TCons t0 t1) t))→(land (nfs2 c (TCons t0 t1)) (nf2 c t))
          we proved (nfs2 c (TApp ts t))→(land (nfs2 c ts) (nf2 c t))
       we proved ∀c:C.∀t:T.∀ts:TList.(nfs2 c (TApp ts t))→(land (nfs2 c ts) (nf2 c t))