(forall
(x)
(iff
(Universal x
)
(exists
(x1)
(Instantiates x x1)
)
)
)
;; Comment: definition of Universal as the domain of Instantiates
(forall
((x Universal))
(not
(x)
)
)
(forall
((x Universal) y z ...s)
(not
(x y z ...s)
)
)
;; Comment: universals are unary
see CUO