 Solution

Equality introduction rule is reflexivity; equality elimination rule permits substitution of equals in a formula:Terms substituted into $\varphi$ must be free for substitution, so no variable becomes captured. The notation $\varphi (s),\varphi (t)$ means substitution into the same designated free variable positions of one formula; other occurrences may remain fixed. These rules express first-order equality without assuming symmetry or transitivity as additional axioms.