For the algorithms, forall(e, phi) and exists(e, phi), phi can be an arbitrary BDD, but e is a conjunction of the variables. The recursive calls will either be done with the same BDD e or with its positive cofactor. Hence, it may finally end up with leaf node True, but never with leaf node False.

Moreover, if phi is a leaf node, then the result is phi since the definition of the quantification is the conjunction or disjunction of the cofactors which are however for constants just the constant itself. As we have x&x=x and x|x=x, this is just phi.