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