theorem cbvrlam {x y: nat} (a: nat x y) (b: nat x) (c: nat y): $ x = y -> b = c $ > $ \. x e. a, b = \. y e. a, c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnv | FN/ y b |
|
2 | nfnv | FN/ x c |
|
3 | hyp e | x = y -> b = c |
|
4 | 1, 2, 3 | cbvrlamh | \. x e. a, b = \. y e. a, c |