theorem nfnlem {x y: nat} (b: nat y) (a c: nat x): $ y = a -> b = c $ > $ FN/ x a $ > $ FN/ x c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqcom | N[a / y] b = c -> c = N[a / y] b |
|
2 | hyp e | y = a -> b = c |
|
3 | 2 | sbne | N[a / y] b = c |
4 | 1, 3 | ax_mp | c = N[a / y] b |
5 | hyp h | FN/ x a |
|
6 | nfnv | FN/ x b |
|
7 | 5, 6 | nfsbnh | FN/ x N[a / y] b |
8 | 4, 7 | nfnx | FN/ x c |