for x, y being LD-EqClass holds
( x '=' y is LD-provable iff x = y )