theorem nfsbs {x y: nat} (a: nat) (A: set x y): $ FS/ x A $ > $ FS/ x S[a / y] A $;
FN/ x a
FS/ x A
FS/ x S[a / y] A