Logical implication defined via if.
Since implies is a function, guards in the consequent must be
verified without assuming the antecedent. impliez is a macro that expands
to an if, so guards in the consequent can be verified assuming the
Definitions and Theorems
(defmacro impliez (p q)
(cons 'if (cons p (cons q '(t)))))