theorem sbset {x: nat} (a: nat) (A: set x) (B: set): $ A. x (x = a -> A == B) -> S[a / x] A == B $;
FS/ x B
A. x (x = a -> A == B) -> S[a / x] A == B