randomb reduces the nondeterministic assignment [x:=*]p(x) to ∀x p(x), because p(x) is true after all ways of assigning any value to x iff p(x) is true for all real values of x.

Other tactics such as chase and unfold also use this axiom.