4vs-implies
(4vs-implies a b) constructs a new sexpr representing (implies a
b).
This is just an abbreviation for (or (not a) b), so we
leave it enabled.
Definitions and Theorems
Function: 4vs-implies
(defun 4vs-implies (a b)
(declare (xargs :guard t))
(4vs-or (4vs-not a) b))
