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