theorem lameqi {x: nat} (a b: nat x): $ a = b $ > $ \ x, a == \ x, b $;
A. x a = b -> \ x, a == \ x, b
a = b
A. x a = b
\ x, a == \ x, b