theorem cbvlams {x y: nat} (a: nat x): $ \ x, a == \ y, N[y / x] a $;
FN/ y a
FN/ x N[y / x] a
x = y -> a = N[y / x] a
\ x, a == \ y, N[y / x] a