theorem nfsbn {x y: nat} (a: nat) (b: nat x y): $ FN/ x b $ > $ FN/ x N[a / y] b $;
FN/ x a
FN/ x b
FN/ x N[a / y] b