for t, u, v being GRZ-formula st t '=' u is LD-provable & u '=' v is LD-provable holds
t '=' v is LD-provable