DEFINITION nfs2()
TYPE =
       C→TList→Prop
BODY =
FIXnfs2{
         nfs2:C→TList→Prop
         :=λc:C
           .λts:TList
             .<λt:TList.Prop> CASE ts OF TNil⇒True | TCons t ts0⇒land (nf2 c t) (nfs2 c ts0)
         }