DEFINITION IsSucc()
TYPE =
       nat→Prop
BODY =
λn:nat.<λn1:nat.Prop> CASE n OF O⇒False | S ⇒True