theorem nfsab {x y: nat} (A: set x y): $ FS/ y A $ > $ FS/ y S\ x, A $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h | FS/ y A |
|
2 | 1 | nfsbs | FS/ y S[fst a1 / x] A |
3 | 2 | nfel2 | F/ y snd a1 e. S[fst a1 / x] A |
4 | 3 | nfab | FS/ y {a1 | snd a1 e. S[fst a1 / x] A} |
5 | 4 | conv sab | FS/ y S\ x, A |