for p, q being MP-variable st @ p = @ q holds
p = q