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.