(a4vec-x) return an a4vec that evaluates to 4vec-x under every environment.
Macro: a4vec-x
(defmacro a4vec-x nil (list 'quote (a4vec (aig-sterm t) (aig-sterm nil))))
Theorem: a4vec-x-correct
(defthm a4vec-x-correct (equal (a4vec-eval (a4vec-x) env) (4vec-x)))
