theorem cbvlam {x y: nat} (a: nat x) (b: nat y): $ x = y -> a = b $ > $ \ x, a == \ y, b $;
FN/ y a
FN/ x b
x = y -> a = b
\ x, a == \ y, b