theorem appneq1d (G: wff) (f g x: nat): $ G -> f = g $ > $ G -> f @ x = g @ x $;
G -> f = g
G -> f == g
G -> f @ x = g @ x