theorem nfsbn1h {x: nat} (a b: nat x): $ FN/ x a $ > $ FN/ x N[a / x] b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hyp h | FN/ x a |
|
| 2 | 1 | nfsb1h | F/ x [a / x] y = b |
| 3 | 2 | nfab | FS/ x {y | [a / x] y = b} |
| 4 | 3 | nfthe | FN/ x the {y | [a / x] y = b} |
| 5 | 4 | conv sbn | FN/ x N[a / x] b |