(defmacro define-symbolic-types (&rest names)
  (let ((types (make-hash-table)))
    (dotimes (n (1+ (length names)))
      (alexandria:map-combinations (lambda (combination)
                                     (let ((name (gensym)))
                                       (dolist (c combination)
                                         (push name (gethash c types '())))))
                                   names
                                   :length n))
    `(progn
       ,@(loop for name in names
               for symbols = (gethash name types)
               collect `(deftype ,name ()
                          '(member ,@symbols)))
       (values-list ',names))))

(defun true? (p) 
  "Is P the universal set, i.e. is our statement P true?"
  (values (subtypep 't p)))

(deftype implies (p q) 
  "Are all elements of P elements of Q? (This is basically SUBTYPEP again.)"
  `(or (not ,p) ,q))

(deftype equals (p q) 
  `(and (implies ,p ,q)
        (implies ,q ,p)))

(define-symbolic-types a b c)
(print (true? '(implies a a)))
(print (true? '(implies a b)))
(print (true? '(implies (and a (implies a b)) b)))
(print (true? '(equals (and a b)
                       (not (or (not a) (not b))))))