Universal quantification of a formula phi over a variable x is defined as the conjunction of the cofactors on that variable, i.e., phi[x<-true] & phi[x<-false]. You can also reduce it to the existential quantification as follows: Forall(x1...xn,phi) = not(Exists(x1...xn,not phi) and then you can use the Exists algorithm as you find it in the slides. Another alternative is to implement the Forall algorithm as the dual of the Exists algorithm (it is essentially the same except that for using Apply with a disjunction you need Apply with a conjunction).
