for x, y being Variable holds
( Var1 (x '=' y) = x & Var2 (x '=' y) = y )