Raw construtor for UBDDs.
(qcons x y) constructs the UBDD whose true branch is x and whose false branch is y. It handles any collapsing which needs to occur.
Function: qcons$inline
(defun qcons$inline (x y) (declare (xargs :guard t)) (if (if (eq x t) (eq y t) (and (eq x nil) (eq y nil))) x (hons x y)))
