theorem cbvals {x y: nat} (p: wff x): $ A. x p <-> A. y [y / x] p $;
F/ y p
F/ x [y / x] p
x = y -> (p <-> [y / x] p)
A. x p <-> A. y [y / x] p