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