theorem eqeqmd (G: wff) (a b n: nat): $ G -> a = b $ > $ G -> mod(n): a = b $;
a = b -> mod(n): a = b
G -> a = b
G -> mod(n): a = b