theorem nfrlam1 {x: nat} (a b: nat x): $ FN/ x a $ > $ FN/ x \. x e. a, b $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nflam1 | FS/ x \ x, b |
|
2 | hyp h1 | FN/ x a |
|
3 | 2 | nfns | FS/ x a |
4 | 1, 3 | nfres | FS/ x (\ x, b) |` a |
5 | 4 | nflower | FN/ x lower ((\ x, b) |` a) |
6 | 5 | conv rlam | FN/ x \. x e. a, b |