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