Universal quantification on a boolean variable x is defined as the conjunction of the cofactors on that variable x. The BDD n6 is the set of variables we quantify over, so that we have to recursively use the high node in case we traverse its root. Have a look at the algorithm posted below:
In case label(e)=label(phi), we call Apply(CONJ,...) with Forall(high(e),high(phi)) and Forall(high(e),low(phi)). In both cases, we have high(e) since that represents the variables {b} which are the ones left after having quantified over a.
