DEFINITION nfs2_tapp()
TYPE =
       ∀c:C.∀t:T.∀ts:TList.(nfs2 c (TApp ts t))→(land (nfs2 c ts) (nf2 c t))
BODY =
Show proof