theorem eqzeqmd (G: wff) (a b n: nat): $ G -> a = b $ > $ G -> modZ(n): a = b $;
a = b -> modZ(n): a = b
G -> a = b
G -> modZ(n): a = b