= Solution
The <equality introduction rule> is reflexivity, with no premise. The <equality elimination rule> is substitution of equal <first-order terms> into a <first-order formula>:
$$
\boxed{\frac{}{\Gamma\vdash t=t}\ =I,\qquad
\frac{\Gamma\vdash s=t\qquad\Gamma\vdash\phi(s)}{\Gamma\vdash\phi(t)}\ =E.}
$$
The indicated substitution must be <capture-avoiding substitution in first-order logic>: the <first-order terms> must be free for the replaced variable. One can designate a particular argument occurrence by choosing $\phi(v)$ appropriately; the rule does not demand replacing every occurrence of an identical-looking term in a formula.
Back to article page
