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