theorem nflam {x y: nat} (a: nat x y): $ FN/ x a $ > $ FS/ x \ y, a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnv | FN/ x p |
|
2 | nfnv | FN/ x y |
|
3 | hyp h | FN/ x a |
|
4 | 2, 3 | nfpr | FN/ x y, a |
5 | 1, 4 | nf_eq | F/ x p = y, a |
6 | 5 | nfex | F/ x E. y p = y, a |
7 | 6 | nfab | FS/ x {p | E. y p = y, a} |
8 | 7 | conv lam | FS/ x \ y, a |