theorem nfsuc {x: nat} (a: nat x): $ FN/ x a $ > $ FN/ x suc a $;
y = a -> suc y = suc a
FN/ x a
FN/ x suc a