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