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