theorem cbvrlams {x y: nat} (a: nat x y) (b: nat x):
$ \. x e. a, b = \. y e. a, N[y / x] b $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfnv | FN/ y b |
|
| 2 | nfsbn1 | FN/ x N[y / x] b |
|
| 3 | sbnq | x = y -> b = N[y / x] b |
|
| 4 | 1, 2, 3 | cbvrlamh | \. x e. a, b = \. y e. a, N[y / x] b |