for t being GRZ-formula holds t '=' t is LD-provable