In that case, you also may draw a horizontal line between variables {a,b} and {c,d}. Then, the existential quantification is "forwarded" by the recursive calls to the BDDs at the line where {c,d} nodes start, and will compute a disjunction there. The result will be the 0-leaf for the 0-leaf and the 1-leaf for others. For instance, if we would just quantify over d in the above BDD, it would replace the d-node by the 1-leaf. As a further consequence, the rightmost c-node will be eliminated since it is then a redundant case distinction.